Bounded Quantifier Instantiation for Checking Inductive Invariants
No abstract available.
DOI 10.1007/978-3-662-54577-5_5
Related papers
- Maximal Quantified Precondition Synthesis for Linear Array Loops ESOP 2024
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays TACAS 2021
- Progress in Certifying Hardware Model Checking Results CAV 2021
- Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion TACAS 2022
- Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy PLDI 2026
- Foundations for natural proofs and quantifier instantiation POPL 2018
- Safety Verification and Refutation by k-Invariants and k-Induction SAS 2015
- Ivy: safety verification by interactive generalization PLDI 2016