Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions

DOI10.1145/3230639MaRDI QIDQ4691738zbMATH OpenOpenAlexWikidataFDO

Authors Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, Roberto Sebastiani

Publication date 24 October 2018

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3230639

zbMATH Keywords

formal verificationnonlinear arithmeticsatisfiability modulo theoriesSMTsymbolic computationtranscendental functions

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Satisfiability modulo transcendental functions via incremental linearization
• Experimenting on solving nonlinear integer arithmetic with incremental linearization
• dReal: an SMT solver for nonlinear theories over the reals
• Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
• Satisfiability of non-linear (ir)rational arithmetic

Cited in

(32)

• Experimenting on solving nonlinear integer arithmetic with incremental linearization
• Subtropical satisfiability
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Towards satisfiability modulo parametric bit-vectors
• The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
• Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
• The SAT+CAS method for combinatorial search with applications to best matrices
• Towards bit-width-independent proofs in SMT solvers
• A non-linear arithmetic procedure for control-command software verification
• Satisfiability modulo transcendental functions via incremental linearization
• -complete decision procedures for satisfiability over the reals
• Satisfiability of non-linear (ir)rational arithmetic
• Superposition modulo non-linear arithmetic
• Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
• dReal: an SMT solver for nonlinear theories over the reals
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• Verification Modulo theories
• Deciding first-order formulas involving univariate mixed trigonometric-polynomials
• The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints
• Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
• Distilling Constraints in Zero-Knowledge Protocols
• Local search for solving satisfiability of polynomial formulas
• Satisfiability modulo finite fields
• More is less: adding polynomials for faster explanations in NLSAT
• Boosting MCSat modulo nonlinear integer arithmetic via local search
• Satisfiability of non-linear transcendental arithmetic as a certificate search problem
• VIRAS: conflict-driven quantifier elimination for integer-real arithmetic
• On the complexity of convex and reverse convex prequadratic constraints
• Satisfiability modulo exponential integer arithmetic
• Optimization modulo non-linear arithmetic via incremental linearization
• Implicit semi-algebraic abstraction for polynomial dynamical systems

Describes a project that uses

Uses Software

• nuXmv
• MathSAT

This page was built for publication: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4691738)