Cited in
(98)- DiffRNN
- FPTaylor
- DyverseRBT
- Deductive verification of floating-point Java programs in KeY
- Hybrid multirate PALS
- Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications
- Computing compositional proofs of input-to-output stability using SOS optimization and \(\delta\)-decidability
- Tropical abstraction of biochemical reaction networks with guarantees
- Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans
- Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties
- Computing the average inter-sample time of event-triggered control using quantitative automata
- Introducing interval differential dynamic logic
- Generating invariants for non-linear hybrid systems
- Implicit definitions with differential equations for KeYmaera X (system description)
- ProbReach: verified probabilistic delta-reachability for stochastic hybrid systems
- Certified roundoff error bounds using semidefinite programming
- SAT modulo discrete event simulation applied to railway design capacity analysis
- NeuroDiff
- ReluDiff
- An approximation framework for solvers and decision procedures
- Rigorous floating-point mixed-precision tuning
- dd
- POPQORN
- ReachNN
- DiffRNN: differential verification of recurrent neural networks
- Optimization modulo non-linear arithmetic via incremental linearization
- Quasi-dependent variables in hybrid automata
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- Zephyrus2
- A non-linear arithmetic procedure for control-command software verification
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
- Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
- raSAT: an SMT solver for polynomial constraints
- Automated deduction -- CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9--14, 2013. Proceedings
- Risk-averse autonomous systems: a brief history and recent developments from the perspective of optimal control
- ModelPlex: verified runtime validation of verified cyber-physical system models
- Minimal-model-guided approaches to solving polynomial constraints and extensions
- Automated and sound synthesis of Lyapunov functions with SMT solvers
- MetiTarski
- QEPCAD
- HySAT
- KeYmaera
- VSDP
- REDLOG
- RSOLVER
- 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
- RangeLab
- Validating numerical semidefinite programming solvers for polynomial invariants
- Daisy
- helperOC
- KeYmaera X
- First-order stable model semantics with intensional functions
- Rigorous roundoff error analysis of probabilistic floating-point computations
- Exploring approximations for floating-point arithmetic using UppSAT
- Construction of parametric barrier functions for dynamical systems using interval analysis
- A search-based procedure for nonlinear real arithmetic
- Barrier certificates revisited
- SMC: satisfiability modulo convex optimization
- raSAT: An SMT Solver for Polynomial Constraints
- Satisfiability modulo theories
This page was built for software: dReal
