Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
From MaRDI portal
Publication:6160909
DOI10.1007/978-3-031-19992-9_9zbMath1522.68716OpenAlexW4312267877MaRDI QIDQ6160909
Alberto Griggio, Enrico Lipparini, Roberto Sebastiani, Alessandro Cimatti
Publication date: 2 June 2023
Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)
Full work available at URL: https://hdl.handle.net/11572/369588
Nonlinear programming (90C30) Degree, winding number (55M25) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- raSAT: an SMT solver for polynomial constraints
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Quasi-decidability of a fragment of the first-order theory of real numbers
- The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
- Safety verification of non-linear hybrid systems is quasi-decidable
- δ-Complete Decision Procedures for Satisfiability over the Reals
- A Model-Constructing Satisfiability Calculus
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- Algorithm 852
- Introduction to Interval Analysis
- Computation of Topological Degree Using Interval Arithmetic, and Applications
- Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
- dReal: An SMT Solver for Nonlinear Theories over the Reals
- Effective topological degree computation based on interval arithmetic
- Understanding the Hastings Algorithm
- Interval Methods for Systems of Equations
- The MathSAT5 SMT Solver
- Some undecidable problems involving elementary functions of a real variable
