Pages that link to "Item:Q4928439"

The following pages link to dReal: An SMT Solver for Nonlinear Theories over the Reals (Q4928439):

Displaying 33 items.

• dReal (Q19210) (← links)
• 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)
• Automated and formal synthesis of neural barrier certificates for dynamical models (Q2044214) (← 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)
• 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)
• Satisfiability Modulo Theories (Q3176369) (← links)
• Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF (Q3303890) (← links)
• Representing hybrid automata by action language modulo theories (Q4592716) (← links)
• Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers (Q5039505) (← links)
• Efficient choice of parameters on delta-reachability bounded hybrid systems (Q5097076) (← 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)