Loop Verification with Invariants and Contracts
No abstract available.
Related papers
- Modular reasoning about heap paths via effectively propositional formulas POPL 2014
- Horn-ICE learning for synthesizing invariants and contracts OOPSLA 2018
- Decidable verification of uninterpreted programs POPL 2019
- Fast and Reliable Formal Verification of Smart Contracts with the Move Prover TACAS 2022
- Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration ESOP 2025
- Verification Modulo Tested Library Contracts PLDI 2026
- Invariant Synthesis for Incomplete Verification Engines TACAS 2018
- Predicate abstraction for software verification POPL 2002