Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
DOI10.1007/978-3-642-32347-8_26zbMATH Open1360.68753OpenAlexW56092462MaRDI QIDQ2914756FDOQ2914756
Publication date: 20 September 2012
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-32347-8_26
Recommendations
- scientific article; zbMATH DE number 953026
- Publication:4203812
- Symbolic computation for the qualitative theory of differential equations
- Numerical Analysis of Ordinary Differential Equations and Its Applications
- scientific article
- Numerical methods and existence theorems for ordinary differential equations
- Characterizing Computable Analysis with Differential Equations
- Affine systems of ODEs in Isabelle/HOL for hybrid-program verification
ordinary differential equationnumerical analysisEuler methodformalization of mathematicsIsabelle/HOLone-step method
Initial value problems, existence, uniqueness, continuous dependence and continuation of solutions to ordinary differential equations (34A12) Software, source code, etc. for problems pertaining to ordinary differential equations (34-04)
Cited In (17)
- The Flow of ODEs
- Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms
- A formalization of metric spaces in HOL Light
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- A Coq formalization of Lebesgue integration of nonnegative functions
- Formally-verified round-off error analysis of Runge-Kutta methods
- The flow of ODEs: formalization of variational equation and Poincaré map
- On the formalization of the heat conduction problem in HOL
- Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
- A verified ODE solver and the Lorenz attractor
- Quantitative continuity and Computable Analysis in Coq
- Title not available (Why is that?)
- Formalization of real analysis: a survey of proof assistants and libraries
- A Verified Enclosure for the Lorenz Attractor (Rough Diamond)
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
- Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method
- The Picard Algorithm for Ordinary Differential Equations in Coq
Uses Software
This page was built for publication: Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2914756)
