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