Constraint Solving for Interpolation

DOI10.1007/978-3-540-69738-1_25zbMath1132.68480OpenAlexW1546818998MaRDI QIDQ5452619

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

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

Related Items

Preface: Special issue on interpolation, Labelled interpolation systems for hyper-resolution, clausal, and local proofs, Guiding Craig interpolation with domain-specific abstractions, A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints, Sharper and Simpler Nonlinear Interpolants for Program Verification, Constraint solving for interpolation, Interpolation Results for Arrays with Length and MaxDiff, An interpolating sequent calculus for quantifier-free Presburger arithmetic, Complete instantiation-based interpolation, Interpolants for Linear Arithmetic in SMT, Model checking duration calculus: a practical approach, Farkas-based tree interpolation, Rewriting Interpolants, Interpolation and Symbol Elimination in Vampire, An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic, Interpolant Generation for UTVPI, Ground Interpolation for Combined Theories, Interpolation and Symbol Elimination, Challenges in Constraint-Based Analysis of Hybrid Systems, Efficient Interpolant Generation in Satisfiability Modulo Theories, Automatically Refining Abstract Interpretations, Distributed and Predictable Software Model Checking, NIL: learning nonlinear interpolants, Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations, Automatic Verification of Combined Specifications: An Overview