An interpolating theorem prover
From MaRDI portal
Publication:2575736
DOI10.1016/j.tcs.2005.07.003zbMath1079.68092OpenAlexW2084294613MaRDI QIDQ2575736
Publication date: 6 December 2005
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2005.07.003
Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40)
Related Items
Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic, Preface: Special issue on interpolation, Labelled interpolation systems for hyper-resolution, clausal, and local proofs, Proof tree preserving tree interpolation, Interpolation systems for ground proofs in automated deduction: a survey, Interpolation and model checking for nonlinear arithmetic, Latticed \(k\)-induction with an application to probabilistic programs, Craig Interpolation in the Presence of Non-linear Constraints, A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints, Satisfiability Modulo Theories, Interpolation and Model Checking, Constraint solving for interpolation, Craig interpolation with clausal first-order tableaux, SMT-based verification of program changes through summary repair, Equality detection for linear arithmetic constraints, Synthesizing history and prophecy variables for symbolic model checking, Probabilistic CEGAR, An interpolating sequent calculus for quantifier-free Presburger arithmetic, Unnamed Item, Unnamed Item, Complete instantiation-based interpolation, Preservation of Craig interpolation by the product of matrix logics, On Interpolation in Decision Procedures, Parallelizing SMT solving: lazy decomposition and conciliation, Quantifier-free interpolation in combinations of equality interpolating theories, Experience of improving the BLAST static verification tool, Craig interpolation in the presence of unreliable connectives, Competent predicate abstraction in model checking, An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic, Interpolant Generation for UTVPI, Ground Interpolation for Combined Theories, Challenges in Constraint-Based Analysis of Hybrid Systems, Efficient Unlinkable Sanitizable Signatures from Signatures with Re-randomizable Keys, Ground Interpolation for the Theory of Equality, Efficient Interpolant Generation in Satisfiability Modulo Theories, Accelerating Interpolation-Based Model-Checking, Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic, Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic, Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference, Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF, Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic, Interpolation in computing science: The semantics of modularization, A Survey of Satisfiability Modulo Theory, Abstract Counterexamples for Non-disjunctive Abstractions, On interpolation in automated theorem proving
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- A structure-preserving clause form translation
- Symbolic model checking: \(10^{20}\) states and beyond
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Abstractions from proofs
- Simplification by Cooperating Decision Procedures
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- GRASP: a search algorithm for propositional satisfiability
- Computer Aided Verification
- Computer Aided Verification
