Interpolant Generation for UTVPI
From MaRDI portal
Publication:5191101
DOI10.1007/978-3-642-02959-2_15zbMath1250.68186OpenAlexW1528842614WikidataQ62041264 ScholiaQ62041264MaRDI QIDQ5191101
Alberto Griggio, Alessandro Cimatti, Roberto Sebastiani
Publication date: 28 July 2009
Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_15
Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40)
Related Items (7)
Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic ⋮ Interpolation and Model Checking ⋮ Constraint solving for interpolation ⋮ Living without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions ⋮ An interpolating sequent calculus for quantifier-free Presburger arithmetic ⋮ On Interpolation in Decision Procedures ⋮ An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
Uses Software
Cites Work
- Unnamed Item
- An interpolating theorem prover
- Abstractions from proofs
- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
- Interpolation in Local Theory Extensions
- Ground Interpolation for the Theory of Equality
- Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
- Computer Aided Verification
- Automated Deduction – CADE-20
- Constraint Solving for Interpolation
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Frontiers of Combining Systems
- Computer Aided Verification
- Fast and Flexible Difference Constraint Propagation for DPLL(T)
- Lazy Abstraction with Interpolants
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Computer Aided Verification
This page was built for publication: Interpolant Generation for UTVPI
