Structural Abstraction of Software Verification Conditions
No abstract available.
Related papers
- Verification of semantic commutativity conditions and inverse operations on linked data structures PLDI 2011
- Program verification using templates over predicate abstraction PLDI 2009
- Full functional verification of linked data structures PLDI 2008
- Formally Validating a Practical Verification Condition Generator CAV 2021
- Null dereference verification via over-approximated weakest pre-conditions analysis OOPSLA 2011
- Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM TACAS 2025
- Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions ECOOP 2013
- Structurally Defined Conditional Data-Flow Static Analysis TACAS 2018