Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement
Abstract elided by the publisher.
Related papers
- Race checking by context inference PLDI 2004
- A Verified Compiler for Probability Density Functions ESOP 2015
- Predicate abstraction and refinement for verifying multi-threaded programs POPL 2011
- Predicate abstraction and CEGAR for higher-order model checking PLDI 2011
- On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem ESOP 2020
- jStar: towards practical verification for java OOPSLA 2008
- Nested refinements: a logic for duck typing POPL 2012
- A refinement hierarchy for free list memory allocators ISMM 2017