Simplifying Loop Invariant Generation Using Splitter Predicates
No abstract available.
Related papers
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference TACAS 2011
- Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop CAV 2006
- Predicate abstraction for software verification POPL 2002
- Inductive Predicate Synthesis Modulo Programs ECOOP 2024
- A Generalized Iterative Construct and Its Semantics TOPLAS 1987
- Path invariants PLDI 2007
- This is the moment for probabilistic loops OOPSLA 2022
- Contextual refinement of the Michael-Scott queue (proof pearl) CPP 2021