Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL

DOI10.1007/978-3-642-32347-8_26MaRDI QIDQ2914756zbMATHOpenAlexFDO

Authors Fabian Immler, Johannes Hölzl

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

zbMATH Keywords

ordinary differential equationnumerical analysisEuler methodformalization of mathematicsIsabelle/HOLone-step method

Mathematics Subject Classification ID

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)

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; zbMATH DE number 49220
• 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

Cited in

(18)

• Formalization of real analysis: a survey of proof assistants and libraries
• Formally-verified round-off error analysis of Runge-Kutta methods
• A verified ODE solver and the Lorenz attractor
• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
• Computable analysis and notions of continuity in \textsc{Coq}
• Affine systems of ODEs in Isabelle/HOL for hybrid-program verification
• The Picard Algorithm for Ordinary Differential Equations in Coq
• Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms
• A Coq formalization of Lebesgue integration of nonnegative functions
• Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
• On the formalization of the heat conduction problem in HOL
• The flow of ODEs
• A formalization of metric spaces in HOL Light
• A verified enclosure for the Lorenz attractor (rough diamond)
• Quantitative continuity and Computable Analysis in Coq
• Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms
• Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method
• The flow of ODEs: formalization of variational equation and Poincaré map

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• Isabelle/Isar
• Flyspeck
• Ordinary Differential Equations

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)