Quantified Invariant Generation Using an Interpolating Saturation Prover
From MaRDI portal
Publication:5458341
DOI10.1007/978-3-540-78800-3_31zbMATH Open1134.68416OpenAlexW1517192598MaRDI QIDQ5458341FDOQ5458341
Authors: K. L. McMillan 
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
Recommendations
Cited In (32)
- Interpolation and model checking for nonlinear arithmetic
- Quantifiers on demand
- Abstract Counterexamples for Non-disjunctive Abstractions
- Abstraction Refinement for Quantified Array Assertions
- Automated verification of functional correctness of race-free GPU programs
- Interpolation and Symbol Elimination
- Invariant relations for affine loops
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs
- Interpolation systems for ground proofs in automated deduction: a survey
- Interpolation and model checking
- Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
- An extension of lazy abstraction with interpolation for programs with arrays
- Machine-checked interpolation theorems for substructural logics using display calculi
- Guiding Craig interpolation with domain-specific abstractions
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- NIL: learning nonlinear interpolants
- Complete instantiation-based interpolation
- Constraint solving for interpolation
- Convergence: integrating termination and abort-freedom
- Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
- Refinement of Trace Abstraction
- Interpolation and symbol elimination in Vampire
- Beyond quantifier-free interpolation in extensions of Presburger arithmetic
- On interpolation in decision procedures
- Craig interpolation in displayable logics
- Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
- Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
- On interpolation in automated theorem proving
- Lingva: generating and proving program properties using symbol elimination
- Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
Uses Software
This page was built for publication: Quantified Invariant Generation Using an Interpolating Saturation Prover
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5458341)
