The following pages link to dReal (Q19210):
Displaying 39 items.
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems (Q287269) (← links)
- Barrier certificates revisited (Q507352) (← links)
- Construction of parametric barrier functions for dynamical systems using interval analysis (Q518335) (← links)
- A search-based procedure for nonlinear real arithmetic (Q518407) (← links)
- ModelPlex: verified runtime validation of verified cyber-physical system models (Q681465) (← links)
- Optimization modulo non-linear arithmetic via incremental linearization (Q831943) (← links)
- DiffRNN: differential verification of recurrent neural networks (Q832044) (← links)
- Rigorous roundoff error analysis of probabilistic floating-point computations (Q832297) (← links)
- raSAT: an SMT solver for polynomial constraints (Q1688535) (← links)
- Exploring approximations for floating-point arithmetic using UppSAT (Q1799086) (← links)
- Automated deduction -- CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9--14, 2013. Proceedings (Q1953299) (← links)
- SAT modulo discrete event simulation applied to railway design capacity analysis (Q2058381) (← links)
- Risk-averse autonomous systems: a brief history and recent developments from the perspective of optimal control (Q2082497) (← links)
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description) (Q2104500) (← links)
- Implicit definitions with differential equations for KeYmaera X (system description) (Q2104559) (← links)
- Formal synthesis of closed-form sampled-data controllers for nonlinear continuous-time systems under STL specifications (Q2116657) (← links)
- Introducing interval differential dynamic logic (Q2145261) (← links)
- Tropical abstraction of biochemical reaction networks with guarantees (Q2229132) (← links)
- Deductive verification of floating-point Java programs in KeY (Q2233510) (← links)
- First-order stable model semantics with intensional functions (Q2321299) (← links)
- A non-linear arithmetic procedure for control-command software verification (Q2324228) (← links)
- Generating invariants for non-linear hybrid systems (Q2355695) (← links)
- An approximation framework for solvers and decision procedures (Q2362497) (← links)
- Computing compositional proofs of input-to-output stability using SOS optimization and \(\delta\)-decidability (Q2374569) (← links)
- Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans (Q2422015) (← links)
- Computing the average inter-sample time of event-triggered control using quantitative automata (Q2677100) (← links)
- raSAT: An SMT Solver for Polynomial Constraints (Q2817923) (← links)
- Hybrid Multirate PALS (Q2945702) (← links)
- Quasi-dependent variables in hybrid automata (Q2986955) (← links)
- ProbReach (Q2988926) (← links)
- Certified Roundoff Error Bounds Using Semidefinite Programming (Q3133585) (← links)
- Satisfiability Modulo Theories (Q3176369) (← links)
- Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions (Q3192080) (← links)
- Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF (Q3303890) (← links)
- Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers (Q5039505) (← links)
- SMC (Q5275314) (← links)
- Rigorous floating-point mixed-precision tuning (Q5370868) (← links)
- Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties (Q5861104) (← links)
- Validating numerical semidefinite programming solvers for polynomial invariants (Q5916266) (← links)
