Constraint solving for interpolation
From MaRDI portal
Publication:604394
DOI10.1016/j.jsc.2010.06.005zbMath1213.68389OpenAlexW2108174021MaRDI QIDQ604394
Viorica Sofronie-Stokkermans, Andrey Rybalchenko
Publication date: 10 November 2010
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jsc.2010.06.005
Related Items
Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic ⋮ Satisfiability Modulo Theories ⋮ Interpolation and Model Checking ⋮ Unnamed Item ⋮ Interpolation Results for Arrays with Length and MaxDiff ⋮ Separators in Continuous Petri Nets ⋮ Separators in continuous Petri nets ⋮ Unnamed Item ⋮ Conditional congruence closure over uninterpreted and interpreted symbols ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Quantifier-free interpolation in combinations of equality interpolating theories ⋮ Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic ⋮ Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF ⋮ On Interpolation and Symbol Elimination in Theory Extensions
Uses Software
Cites Work
- Unnamed Item
- The octagon abstract domain
- Model checking duration calculus: a practical approach
- Real addition and the polynomial hierarchy
- An interpolating theorem prover
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Abstractions from proofs
- Model Checking Duration Calculus: A Practical Approach
- Interpolants for Linear Arithmetic in SMT
- Interpolation in Local Theory Extensions
- Interpolation in local theory extensions
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Interpolant Generation for UTVPI
- Ground Interpolation for Combined Theories
- Interpolation and Symbol Elimination
- Automated Deduction – CADE-20
- Automated Deduction – CADE-20
- Constraint Solving for Interpolation
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
- Computer Aided Verification
- Lazy Abstraction with Interpolants
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Computer Aided Verification
- Tractable disjunctions of linear constraints: Basic results and applications to temporal reasoning
