Constraint solving for interpolation
From MaRDI portal
Publication:604394
DOI10.1016/j.jsc.2010.06.005zbMath1213.68389MaRDI 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
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Quantifier-free interpolation in combinations of equality interpolating theories, Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
Uses Software
Cites Work
- 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
- Unnamed Item
