Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
From MaRDI portal
Publication:2914756
DOI10.1007/978-3-642-32347-8_26zbMath1360.68753OpenAlexW56092462MaRDI QIDQ2914756
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
ordinary differential equationEuler methodone-step methodnumerical analysisIsabelle/HOLformalization of mathematics
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (16)
Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ A verified ODE solver and the Lorenz attractor ⋮ A Verified Enclosure for the Lorenz Attractor (Rough Diamond) ⋮ A Coq formalization of Lebesgue integration of nonnegative functions ⋮ Unnamed Item ⋮ 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 ⋮ Formally-verified round-off error analysis of Runge-Kutta methods ⋮ On the formalization of the heat conduction problem in HOL ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms ⋮ The flow of ODEs: formalization of variational equation and Poincaré map ⋮ Quantitative continuity and Computable Analysis in Coq ⋮ A formalization of metric spaces in HOL Light ⋮ Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms ⋮ The Flow of ODEs
Uses Software
This page was built for publication: Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
