Constraint solving for interpolation
From MaRDI portal
Publication:604394
DOI10.1016/J.JSC.2010.06.005zbMATH Open1213.68389OpenAlexW2108174021MaRDI QIDQ604394FDOQ604394
Authors: Andrey Rybalchenko, Viorica Sofronie-Stokkermans 
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
Recommendations
- Constraint Solving for Interpolation
- Lagrange interpolation with constraints
- Approximation with interpolatory constraints
- An Algorithm for Constrained Interpolation
- scientific article; zbMATH DE number 2064510
- Interpolation with multiple norm constraints
- Constrained interpolation and smoothing
- scientific article
- On best constrained interpolation
- Real interpolation with constraints
Cites Work
- The octagon abstract domain
- Title not available (Why is that?)
- Interpolation and SAT-based model checking.
- An interpolating theorem prover
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Abstractions from proofs
- 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
- Ground Interpolation for Combined Theories
- Interpolation and Symbol Elimination
- Automated Deduction – CADE-20
- Constraint Solving for Interpolation
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- 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
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
- Real addition and the polynomial hierarchy
- Interpolant Generation for UTVPI
- Automated Deduction – CADE-20
- Model Checking Duration Calculus: A Practical Approach
- Computer Aided Verification
- Tractable disjunctions of linear constraints: Basic results and applications to temporal reasoning
- Model checking duration calculus: a practical approach
Cited In (24)
- Conditional congruence closure over uninterpreted and interpreted symbols
- An Algorithm for Constrained Interpolation
- Separators in Continuous Petri Nets
- Whale: an interpolation-based algorithm for inter-procedural verification
- Ground Interpolation for Combined Theories
- Parallelizing SMT solving: lazy decomposition and conciliation
- Automated Deduction – CADE-20
- Quantifier-free interpolation in combinations of equality interpolating theories
- Constraint Solving for Interpolation
- Sharper and Simpler Nonlinear Interpolants for Program Verification
- Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
- Separators in continuous Petri nets
- Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
- Title not available (Why is that?)
- Interpolation and Model Checking
- Interpolation Results for Arrays with Length and MaxDiff
- On interpolation in decision procedures
- A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints
- On Interpolation and Symbol Elimination in Theory Extensions
- Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
- Title not available (Why is that?)
- On P-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics $$\mathcal{E}\mathcal{L}, \mathcal{E}\mathcal{L}^+$$
- An interpolating theorem prover
- Satisfiability Modulo Theories
Uses Software
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 Q604394)
