Quantified Invariant Generation Using an Interpolating Saturation Prover
From MaRDI portal
Publication:5458341
DOI10.1007/978-3-540-78800-3_31zbMath1134.68416MaRDI 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
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Interpolation and Symbol Elimination, Complete instantiation-based interpolation, Interpolation and Symbol Elimination in Vampire, Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference, Labelled interpolation systems for hyper-resolution, clausal, and local proofs, Interpolation systems for ground proofs in automated deduction: a survey, Guiding Craig interpolation with domain-specific abstractions, An extension of lazy abstraction with interpolation for programs with arrays, Constraint solving for interpolation, Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists, Convergence: integrating termination and abort-freedom, Automated verification of functional correctness of race-free GPU programs, Counterexample-guided prophecy for model checking modulo the theory of arrays, NIL: learning nonlinear interpolants, On interpolation in automated theorem proving, Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF, Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi, On Interpolation in Decision Procedures, Craig Interpolation in Displayable Logics, Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic, Interpolation and Model Checking, Abstraction Refinement for Quantified Array Assertions, Refinement of Trace Abstraction, A First Class Boolean Sort in First-Order Theorem Proving and TPTP, Lingva: Generating and Proving Program Properties Using Symbol Elimination, Abstract Counterexamples for Non-disjunctive Abstractions
Uses Software
