Quantified Invariant Generation Using an Interpolating Saturation Prover
No abstract available.
Related papers
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic VMCAI 2011
- egg: Fast and extensible equality saturation POPL 2021
- Interpolation and Quantifiers in Ortholattices VMCAI 2024
- A modular Isabelle framework for verifying saturation provers CPP 2021
- An Interpolating Theorem Prover TACAS 2004
- First-order quantified separators PLDI 2020
- QSM-Cutoff: Systematic Derivation of Quantified Cutoff Formulas for Distributed Protocols CAV 2025
- Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation CAV 2015