Interpolation and model checking for nonlinear arithmetic
From MaRDI portal
Publication:832268
DOI10.1007/978-3-030-81688-9_13zbMATH Open1493.68212arXiv2106.04340OpenAlexW3184821935MaRDI QIDQ832268FDOQ832268
Authors: Dejan Jovanović, Bruno Dutertre 
Publication date: 25 March 2022
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.
Full work available at URL: https://arxiv.org/abs/2106.04340
Recommendations
Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)
Cites Work
- Theory and Applications of Satisfiability Testing
- A procedure for proving special function inequalities involving a discrete parameter
- Algorithms in real algebraic geometry
- An interpolating theorem prover
- Solving Non-linear Arithmetic
- A Model-Constructing Satisfiability Calculus
- Satisfiability Modulo Theories
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Abstractions from proofs
- Title not available (Why is that?)
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Generalized Property Directed Reachability
- Title not available (Why is that?)
- Temporal induction by incremental SAT solving
- Generating Non-linear Interpolants by Semidefinite Programming
- SMT-based model checking for recursive programs
- Title not available (Why is that?)
- Efficient interpolation for the theory of arrays
- Solving bitvectors with MCSAT: explanations from bits and pieces
- Nonlinear Craig interpolant generation
- Interpolants in nonlinear theories over the reals
- Constructing a single cell in cylindrical algebraic decomposition
- Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF
- Solving Nonlinear Integer Arithmetic with MCSAT
- Craig interpolation in the presence of non-linear constraints
- Selfless Interpolation for Infinite-State Model Checking
- Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
- Title not available (Why is that?)
- Constructing Craig interpolation formulas
Cited In (2)
Uses Software
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)
