Interpolation and model checking for nonlinear arithmetic
From MaRDI portal
(Redirected from Publication:832268)
Abstract: We present a new model-based interpolation procedure for satisfiability modulo theories (SMT). The procedure uses a new mode of interaction with the SMT solver that we call solving modulo a model. This either extends a given partial model into a full model for a set of assertions or returns an explanation (a model interpolant) when no solution exists. This mode of interaction fits well into the model-constructing satisfiability (MCSAT) framework of SMT. We use it to develop an interpolation procedure for any MCSAT-supported theory. In particular, this method leads to an effective interpolation procedure for nonlinear real arithmetic. We evaluate the new procedure by integrating it into a model checker and comparing it with state-of-art model-checking tools for nonlinear arithmetic.
Recommendations
Cites work
- scientific article; zbMATH DE number 3497890 (Why is no real title available?)
- scientific article; zbMATH DE number 517393 (Why is no real title available?)
- scientific article; zbMATH DE number 1140679 (Why is no real title available?)
- scientific article; zbMATH DE number 6604030 (Why is no real title available?)
- A model-constructing satisfiability calculus
- A procedure for proving special function inequalities involving a discrete parameter
- Abstractions from proofs
- Algorithms in real algebraic geometry
- An interpolating theorem prover
- Constructing Craig interpolation formulas
- Constructing a single cell in cylindrical algebraic decomposition
- Craig interpolation in the presence of non-linear constraints
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Efficient interpolation for the theory of arrays
- Generalized property directed reachability
- Generating non-linear interpolants by semidefinite programming
- Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
- Interpolants in nonlinear theories over the reals
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Nonlinear Craig interpolant generation
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- SMT-based model checking for recursive programs
- Satisfiability modulo theories
- Selfless interpolation for infinite-state model checking
- Solving bitvectors with MCSAT: explanations from bits and pieces
- Solving non-linear arithmetic
- Solving nonlinear integer arithmetic with MCSAT
- Temporal induction by incremental SAT solving
- Theory and Applications of Satisfiability Testing
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
Cited in
(7)- Farkas-based tree interpolation
- Solving nonlinear integer arithmetic with MCSAT
- Selfless interpolation for infinite-state model checking
- NIL: learning nonlinear interpolants
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
- A search-based procedure for nonlinear real arithmetic
- Interpolants for Linear Arithmetic in SMT
This page was built for publication: Interpolation and model checking for nonlinear arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832268)
