Quantified Invariant Generation Using an Interpolating Saturation Prover

DOI10.1007/978-3-540-78800-3_31MaRDI QIDQ5458341zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Quantifier-free interpolation of a theory of arrays
• Tools and Algorithms for the Construction and Analysis of Systems
• An interpolating theorem prover
• An extension of lazy abstraction with interpolation for programs with arrays
• Complete instantiation-based interpolation

Cited in

(32)

• Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference
• Invariant relations for affine loops
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Beyond quantifier-free interpolation in extensions of Presburger arithmetic
• Interpolation and symbol elimination in Vampire
• On interpolation in decision procedures
• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• Complete instantiation-based interpolation
• Interpolation and model checking for nonlinear arithmetic
• Abstract Counterexamples for Non-disjunctive Abstractions
• 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
• Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• Choose Your Colour: Tree Interpolation for Quantified Formulas in SMT
• Lingva: generating and proving program properties using symbol elimination
• Abstraction Refinement for Quantified Array Assertions
• Interpolation and model checking
• Refinement of Trace Abstraction
• Constraint solving for interpolation
• Craig interpolation in displayable logics
• Convergence: integrating termination and abort-freedom
• An extension of lazy abstraction with interpolation for programs with arrays
• Automated verification of functional correctness of race-free GPU programs
• Machine-checked interpolation theorems for substructural logics using display calculi
• On interpolation in automated theorem proving
• Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
• Interpolation and Symbol Elimination
• NIL: learning nonlinear interpolants
• Quantifiers on demand
• Guiding Craig interpolation with domain-specific abstractions

Describes a project that uses

Uses Software

• FOCI

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)