Pages that link to "Item:Q2914756"
From MaRDI portal
The following pages link to Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL (Q2914756):
Displaying 16 items.
- A formalization of metric spaces in HOL Light (Q682381) (← links)
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL (Q832721) (← links)
- A verified ODE solver and the Lorenz attractor (Q1663218) (← links)
- Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms (Q1722642) (← links)
- The flow of ODEs: formalization of variational equation and Poincaré map (Q1722644) (← links)
- Affine systems of ODEs in Isabelle/HOL for hybrid-program verification (Q2038037) (← links)
- A Coq formalization of Lebesgue integration of nonnegative functions (Q2673304) (← links)
- Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms (Q2829257) (← links)
- The Flow of ODEs (Q2829258) (← links)
- A Verified Enclosure for the Lorenz Attractor (Rough Diamond) (Q2945634) (← links)
- Formalization of real analysis: a survey of proof assistants and libraries (Q2973239) (← links)
- (Q4989411) (← links)
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL (Q5098720) (← links)
- The Picard Algorithm for Ordinary Differential Equations in Coq (Q5327365) (← links)
- Quantitative continuity and Computable Analysis in Coq (Q5875440) (← links)
- Formally-verified round-off error analysis of Runge-Kutta methods (Q6149594) (← links)