Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
From MaRDI portal
Publication:4691738
DOI10.1145/3230639zbMath1407.68285OpenAlexW2889414920WikidataQ129283086 ScholiaQ129283086MaRDI QIDQ4691738
Marco Roveri, Alberto Griggio, Ahmed Irfan, Alessandro Cimatti, 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
symbolic computationformal verificationtranscendental functionsSMTsatisfiability modulo theoriesnonlinear arithmetic
Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays, Optimization modulo non-linear arithmetic via incremental linearization, Implicit semi-algebraic abstraction for polynomial dynamical systems, 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, 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, The SAT+CAS method for combinatorial search with applications to best matrices, Towards satisfiability modulo parametric bit-vectors, The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints, Towards bit-width-independent proofs in SMT solvers, Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
Uses Software
