Constraint solving for interpolation
From MaRDI portal
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; zbMATH DE number 124543
- On best constrained interpolation
- Real interpolation with constraints
Cites work
- Abstractions from proofs
- An interpolating theorem prover
- Automated Deduction – CADE-20
- Automated Deduction – CADE-20
- Computer Aided Verification
- Computer Aided Verification
- Computer Aided Verification
- Constraint Solving for Interpolation
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Ground Interpolation for Combined Theories
- scientific article; zbMATH DE number 4089320 (Why is no real title available?)
- Interpolant Generation for UTVPI
- Interpolants for Linear Arithmetic in SMT
- Interpolation and SAT-based model checking.
- Interpolation and Symbol Elimination
- Interpolation in local theory extensions
- Interpolation in Local Theory Extensions
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lazy Abstraction with Interpolants
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Model checking duration calculus: a practical approach
- Model Checking Duration Calculus: A Practical Approach
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Real addition and the polynomial hierarchy
- The octagon abstract domain
- Tools and Algorithms for the Construction and Analysis of Systems
- Tools and Algorithms for the Construction and Analysis of Systems
- Tractable disjunctions of linear constraints: Basic results and applications to temporal reasoning
- Verification, Model Checking, and Abstract Interpretation
Cited in
(38)- Symbolic polytopes for quantitative interpolation and verification
- Conditional congruence closure over uninterpreted and interpreted symbols
- Parallelizing SMT solving: lazy decomposition and conciliation
- Probably approximately correct interpolants generation
- An interpolating theorem prover
- Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
- Generating non-linear interpolants by semidefinite programming
- Proof tree preserving tree interpolation
- PeRIPLO: a framework for producing effective interpolants in SAT-based software verification
- Whale: an interpolation-based algorithm for inter-procedural verification
- Playing in the grey area of proofs
- On interpolation in decision procedures
- A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints
- Satisfiability modulo theories
- Interpolation and model checking
- Improving interpolants for linear arithmetic
- An Algorithm for Constrained Interpolation
- Effectively propositional interpolants
- Partially ordered automata and piecewise testability
- Generalised interpolation by solving recursion-free Horn clauses
- scientific article; zbMATH DE number 7444022 (Why is no real title available?)
- Mind the gap: bit-vector interpolation recast over linear integer arithmetic
- Sharper and Simpler Nonlinear Interpolants for Program Verification
- Abstracting induction by extrapolation and interpolation
- Ground Interpolation for Combined Theories
- Automated Deduction – CADE-20
- Quantifier-free interpolation in combinations of equality interpolating theories
- Rewriting interpolants
- Constraint Solving for Interpolation
- Complete instantiation-based interpolation
- Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
- Interpolation Results for Arrays with Length and MaxDiff
- Decomposing Farkas Interpolants
- Separators in Continuous Petri Nets
- Separators in continuous Petri nets
- 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}^+$$
- On recursion-free Horn clauses and Craig interpolation
- Interpolation and model checking for nonlinear arithmetic
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)
