Constraint Solving for Interpolation
DOI10.1007/978-3-540-69738-1_25zbMATH Open1132.68480OpenAlexW1546818998MaRDI QIDQ5452619FDOQ5452619
Authors: Andrey Rybalchenko, Viorica Sofronie-Stokkermans
Publication date: 4 April 2008
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-69738-1_25
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (47)
- Challenges in Constraint-Based Analysis of Hybrid Systems
- Mind the gap: bit-vector interpolation recast over linear integer arithmetic
- Interpolation and model checking for nonlinear arithmetic
- An Algorithm for Constrained Interpolation
- Effectively propositional interpolants
- Generating non-linear interpolants by semidefinite programming
- Whale: an interpolation-based algorithm for inter-procedural verification
- Farkas-based tree interpolation
- Interpolant Generation for UTVPI
- Ground Interpolation for Combined Theories
- Interpolation and Symbol Elimination
- Abstracting induction by extrapolation and interpolation
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs
- Preface: Special issue on interpolation
- Proof tree preserving tree interpolation
- Automated Deduction – CADE-20
- Quantifier-free interpolation in combinations of equality interpolating theories
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Guiding Craig interpolation with domain-specific abstractions
- Sharper and Simpler Nonlinear Interpolants for Program Verification
- Distributed and predictable software model checking
- NIL: learning nonlinear interpolants
- Complete instantiation-based interpolation
- On recursion-free Horn clauses and Craig interpolation
- Nonlinear Craig interpolant generation
- Complete instantiation-based interpolation
- Constraint solving for interpolation
- Rewriting interpolants
- Model checking duration calculus: a practical approach
- Interpolation Results for Arrays with Length and MaxDiff
- Interpolation and symbol elimination in Vampire
- On interpolation in decision procedures
- A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints
- PeRIPLO: a framework for producing effective interpolants in SAT-based software verification
- Probably approximately correct interpolants generation
- Generalised interpolation by solving recursion-free Horn clauses
- Spatial interpolants
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- Improving interpolants for linear arithmetic
- Playing in the grey area of proofs
- Symbolic polytopes for quantitative interpolation and verification
- Decomposing Farkas Interpolants
- Automatically Refining Abstract Interpretations
- Automatic verification of combined specifications: an overview
- Interpolants for Linear Arithmetic in SMT
This page was built for publication: Constraint Solving for Interpolation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5452619)