Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems
No abstract available.
Related papers
- Contract Soundness for Object-Oriented Languages OOPSLA 2001
- Automatic Verification of Integer Array Programs CAV 2009
- Recursive proofs for inductive tree data-structures POPL 2012
- From Pre-historic to Post-modern Symbolic Model Checking CAV 1998
- Shape Analysis via Second-Order Bi-Abduction CAV 2014
- Logic of global synchrony TOPLAS 2004
- Efficient Algorithms for pre* and post* on Interprocedural Parallel Flow Graphs POPL 2000
- Data-Driven Verification of Procedural Programs with Integer Arrays CAV 2025