swMATH7157MaRDI QIDQ19210FDOQ19210
Author name not available (Why is that?)
Official website: http://dreal.cs.cmu.edu/
Cited In (93)
- DiffRNN
- FPTaylor
- DyverseRBT
- Hybrid multirate PALS
- Tropical abstraction of biochemical reaction networks with guarantees
- Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties
- Deductive verification of floating-point Java programs in KeY
- Computing compositional proofs of input-to-output stability using SOS optimization and \(\delta\)-decidability
- Computing the average inter-sample time of event-triggered control using quantitative automata
- Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans
- Implicit definitions with differential equations for KeYmaera X (system description)
- NeuroDiff
- ReluDiff
- DiffRNN: differential verification of recurrent neural networks
- Optimization modulo non-linear arithmetic via incremental linearization
- Minimal-model-guided approaches to solving polynomial constraints and extensions
- Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications
- dd
- POPQORN
- ReachNN
- SMC: satisfiability modulo convex optimization
- Zephyrus2
- Quasi-dependent variables in hybrid automata
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- Certified roundoff error bounds using semidefinite programming
- Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
- Generating invariants for non-linear hybrid systems
- A non-linear arithmetic procedure for control-command software verification
- Introducing interval differential dynamic logic
- Automated and sound synthesis of Lyapunov functions with SMT solvers
- raSAT: an SMT solver for polynomial constraints
- QEPCAD
- VSDP
- RealPaver
- Gappa
- libpoly
- MATISSE
- Flocq
- NLCertify
- MathSAT5
- PVSio
- CalCS
- TopDeg
- SMT-RAT
- SynchAADL2Maude
- cftool
- raSAT
- FloPoCo
- BFComp
- ManyOpt
- EFSMT
- JBernstein
- Averist
- CyPhySim
- PySMT
- dReach
- Flow*
- HYST
- HyComp
- ProbReach
- AADL
- Stabhyli
- SReach
- ABsolver
- FPTuner
- RailCNL
- lquadmath
- Bellerophon
- SONOLAR
- XSat
- Coq Interval
- Joblib
- Satisfiability modulo theories
- Automated deduction -- CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9--14, 2013. Proceedings
- Rigorous roundoff error analysis of probabilistic floating-point computations
- Exploring approximations for floating-point arithmetic using UppSAT
- RangeLab
- Daisy
- helperOC
- KeYmaera X
- SAT modulo discrete event simulation applied to railway design capacity analysis
- First-order stable model semantics with intensional functions
- An approximation framework for solvers and decision procedures
- Validating numerical semidefinite programming solvers for polynomial invariants
- raSAT: An SMT Solver for Polynomial Constraints
- Risk-averse autonomous systems: a brief history and recent developments from the perspective of optimal control
- Barrier certificates revisited
- Construction of parametric barrier functions for dynamical systems using interval analysis
- A search-based procedure for nonlinear real arithmetic
- ProbReach: verified probabilistic delta-reachability for stochastic hybrid systems
- Rigorous floating-point mixed-precision tuning
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
- ModelPlex: verified runtime validation of verified cyber-physical system models
This page was built for software: dReal
