dReal
From MaRDI portal
DReal
Cited in
(98)- MetiTarski
- QEPCAD
- dd
- ReachNN
- POPQORN
- HySAT
- KeYmaera
- VSDP
- REDLOG
- RSOLVER
- RealPaver
- raSAT: an SMT solver for polynomial constraints
- Gappa
- libpoly
- Exploring approximations for floating-point arithmetic using UppSAT
- MATISSE
- Flocq
- Automated deduction -- CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9--14, 2013. Proceedings
- SAT modulo discrete event simulation applied to railway design capacity analysis
- NLCertify
- 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
- MathSAT5
- 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
- A non-linear arithmetic procedure for control-command software verification
- 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 -decidability
- Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans
- PVSio
- TopDeg
- SMT-RAT
- CalCS
- SynchAADL2Maude
- Computing the average inter-sample time of event-triggered control using quantitative automata
- cftool
- raSAT
- raSAT: An SMT Solver for Polynomial Constraints
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- Hybrid multirate PALS
- Quasi-dependent variables in hybrid automata
- ProbReach: verified probabilistic delta-reachability for stochastic hybrid systems
- FloPoCo
- BFComp
- ManyOpt
- JBernstein
- EFSMT
- Certified roundoff error bounds using semidefinite programming
- PySMT
- Satisfiability modulo theories
- Minimal-model-guided approaches to solving polynomial constraints and extensions
- Stabhyli
- Averist
- HYST
- CyPhySim
- ProbReach
- SReach
- Flow*
- HyComp
- dReach
- AADL
- Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
- ABsolver
- RailCNL
- FPTuner
- lquadmath
- Bellerophon
- XSat
- SONOLAR
- Coq Interval
- Joblib
- Automated and sound synthesis of Lyapunov functions with SMT solvers
- Barrier certificates revisited
- Construction of parametric barrier functions for dynamical systems using interval analysis
- A search-based procedure for nonlinear real arithmetic
- SMC: satisfiability modulo convex optimization
- Rigorous floating-point mixed-precision tuning
- RangeLab
- helperOC
- KeYmaera X
- Daisy
- Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties
- Validating numerical semidefinite programming solvers for polynomial invariants
- NeuroDiff
- ReluDiff
- FPTaylor
- DiffRNN
- Zephyrus2
- DyverseRBT
- 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
This page was built for software: dReal
