dReal: An SMT Solver for Nonlinear Theories over the Reals

DOI10.1007/978-3-642-38574-2_14zbMath1381.68268OpenAlexW2166280160MaRDI QIDQ4928439

Soonho Kong, Sicun Gao, Edmund M. Clarke

Publication date: 14 June 2013

Published in: Automated Deduction – CADE-24 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-38574-2_14

Mathematics Subject Classification ID

Related Items (41)

An approximation framework for solvers and decision procedures ⋮ Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers ⋮ Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems ⋮ Optimization modulo non-linear arithmetic via incremental linearization ⋮ DiffRNN: differential verification of recurrent neural networks ⋮ Rigorous roundoff error analysis of probabilistic floating-point computations ⋮ Computing compositional proofs of input-to-output stability using SOS optimization and \(\delta\)-decidability ⋮ Satisfiability Modulo Theories ⋮ Introducing interval differential dynamic logic ⋮ Hybrid Multirate PALS ⋮ Efficient choice of parameters on delta-reachability bounded hybrid systems ⋮ Computing the average inter-sample time of event-triggered control using quantitative automata ⋮ raSAT: an SMT solver for polynomial constraints ⋮ Representing hybrid automata by action language modulo theories ⋮ Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans ⋮ FOSSIL ⋮ Verifying Switched System Stability With Logic ⋮ Verifying Neural Network Controlled Systems Using Neural Networks ⋮ ETCetera: beyond Event-Triggered Control ⋮ Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test ⋮ Railway scheduling using Boolean satisfiability modulo simulations ⋮ \textsf{symQV}: automated symbolic verification of quantum programs ⋮ Interval Markov Decision Processes with Continuous Action-Spaces ⋮ Tropical abstraction of biochemical reaction networks with guarantees ⋮ Deductive verification of floating-point Java programs in KeY ⋮ Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF ⋮ Barrier certificates revisited ⋮ ModelPlex: verified runtime validation of verified cyber-physical system models ⋮ Construction of parametric barrier functions for dynamical systems using interval analysis ⋮ A search-based procedure for nonlinear real arithmetic ⋮ Validating numerical semidefinite programming solvers for polynomial invariants ⋮ Automated and formal synthesis of neural barrier certificates for dynamical models ⋮ raSAT: An SMT Solver for Polynomial Constraints ⋮ dReal ⋮ First-order stable model semantics with intensional functions ⋮ Risk-averse autonomous systems: a brief history and recent developments from the perspective of optimal control ⋮ Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties ⋮ Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description) ⋮ Implicit definitions with differential equations for KeYmaera X (system description) ⋮ Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications ⋮ Generating invariants for non-linear hybrid systems

Uses Software

• SMT-LIB
• RealPaver
• OpenSMT
• CalCS

This page was built for publication: dReal: An SMT Solver for Nonlinear Theories over the Reals