dReal: An SMT Solver for Nonlinear Theories over the Reals
From MaRDI portal
Publication:4928439
DOI10.1007/978-3-642-38574-2_14zbMath1381.68268MaRDI 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
Related Items
Representing hybrid automata by action language modulo theories, Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers, Efficient choice of parameters on delta-reachability bounded hybrid systems, Validating numerical semidefinite programming solvers for polynomial invariants, Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties, 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, dReal, Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems, Barrier certificates revisited, Construction of parametric barrier functions for dynamical systems using interval analysis, A search-based procedure for nonlinear real arithmetic, ModelPlex: verified runtime validation of verified cyber-physical system models, Optimization modulo non-linear arithmetic via incremental linearization, DiffRNN: differential verification of recurrent neural networks, Rigorous roundoff error analysis of probabilistic floating-point computations, raSAT: an SMT solver for polynomial constraints, Automated and formal synthesis of neural barrier certificates for dynamical models, Risk-averse autonomous systems: a brief history and recent developments from the perspective of optimal control, 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, Introducing interval differential dynamic logic, Tropical abstraction of biochemical reaction networks with guarantees, Deductive verification of floating-point Java programs in KeY, First-order stable model semantics with intensional functions, Generating invariants for non-linear hybrid systems, An approximation framework for solvers and decision procedures, Computing compositional proofs of input-to-output stability using SOS optimization and \(\delta\)-decidability, Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans, Computing the average inter-sample time of event-triggered control using quantitative automata, raSAT: An SMT Solver for Polynomial Constraints, Hybrid Multirate PALS, Satisfiability Modulo Theories, Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
Uses Software
