Constraint Solving for Interpolation

DOI10.1007/978-3-540-69738-1_25MaRDI QIDQ5452619zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Constraint solving for interpolation
• Improving interpolants for linear arithmetic
• An interpolating theorem prover
• Tools and Algorithms for the Construction and Analysis of Systems
• Automated Deduction – CADE-20

Cited in

(47)

• Interpolation and model checking for nonlinear arithmetic
• Mind the gap: bit-vector interpolation recast over linear integer arithmetic
• Challenges in Constraint-Based Analysis of Hybrid Systems
• An Algorithm for Constrained Interpolation
• Generating non-linear interpolants by semidefinite programming
• Effectively propositional interpolants
• Whale: an interpolation-based algorithm for inter-procedural verification
• Farkas-based tree interpolation
• Labelled interpolation systems for hyper-resolution, clausal, and local proofs
• Preface: Special issue on interpolation
• Proof tree preserving tree interpolation
• Interpolant Generation for UTVPI
• Ground Interpolation for Combined Theories
• Interpolation and Symbol Elimination
• Abstracting induction by extrapolation and interpolation
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• Guiding Craig interpolation with domain-specific abstractions
• Automated Deduction – CADE-20
• Quantifier-free interpolation in combinations of equality interpolating theories
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Distributed and predictable software model checking
• NIL: learning nonlinear interpolants
• Sharper and Simpler Nonlinear Interpolants for Program Verification
• On recursion-free Horn clauses and Craig interpolation
• Nonlinear Craig interpolant generation
• Complete instantiation-based interpolation
• Complete instantiation-based interpolation
• Constraint solving for interpolation
• Model checking duration calculus: a practical approach
• Rewriting interpolants
• On interpolation in decision procedures
• A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints
• Interpolation Results for Arrays with Length and MaxDiff
• PeRIPLO: a framework for producing effective interpolants in SAT-based software verification
• Interpolation and symbol elimination in Vampire
• Probably approximately correct interpolants generation
• Generalised interpolation by solving recursion-free Horn clauses
• Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
• Spatial interpolants
• Improving interpolants for linear arithmetic
• Symbolic polytopes for quantitative interpolation and verification
• Playing in the grey area of proofs
• Automatically Refining Abstract Interpretations
• Decomposing Farkas Interpolants
• 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)