Quantified Invariant Generation Using an Interpolating Saturation Prover
From MaRDI portal
Publication:5458341
DOI10.1007/978-3-540-78800-3_31zbMath1134.68416OpenAlexW1517192598MaRDI QIDQ5458341
Publication date: 11 April 2008
Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-78800-3_31
Related Items
Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ Interpolation and model checking for nonlinear arithmetic ⋮ Guiding Craig interpolation with domain-specific abstractions ⋮ A First Class Boolean Sort in First-Order Theorem Proving and TPTP ⋮ Interpolation and Model Checking ⋮ Lingva: Generating and Proving Program Properties Using Symbol Elimination ⋮ Convergence: integrating termination and abort-freedom ⋮ Constraint solving for interpolation ⋮ Automated verification of functional correctness of race-free GPU programs ⋮ Complete instantiation-based interpolation ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ On Interpolation in Decision Procedures ⋮ Craig Interpolation in Displayable Logics ⋮ Interpolation and Symbol Elimination in Vampire ⋮ Interpolation and Symbol Elimination ⋮ Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic ⋮ Counterexample-guided prophecy for model checking modulo the theory of arrays ⋮ Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference ⋮ Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists ⋮ Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF ⋮ Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi ⋮ NIL: learning nonlinear interpolants ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic ⋮ Abstraction Refinement for Quantified Array Assertions ⋮ Refinement of Trace Abstraction ⋮ Abstract Counterexamples for Non-disjunctive Abstractions ⋮ On interpolation in automated theorem proving
Uses Software
