Formally Verified Computation of Enclosures of Solutions of Ordinary Differential Equations
Formally Verified Computation of Enclosures of Solutions of Ordinary Differential Equations
复制标题
常微分方程解围的形式化验证计算
DOI：
10.1007/978-3-319-06200-6_9
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Fabian Immler
中科院分区：
文献类型：
--
作者：
Fabian Immler
在建立连续动力学模型时，常微分方程组是普遍存在的。经典的数值方法计算的是解的近似值，但对近似值的质量没有任何保证。然而，已经发展了一些方法来计算解的包含性。在这篇文章中，我们证明了解的包含性可以以高水平的严密性来验证：我们在交互式定理证明器Isabelle/HOL中实现了一个函数算法来计算常微分方程组的解的包含性，其中我们形式化地验证(并且已经机械地检查)了依莎贝尔/HOL中现有的常微分方程组理论的包含性。我们的算法以静态固定的精度处理二进有理数，并且基于著名的欧拉方法。我们将离散化和舍入误差抽象到仿射形式域中。经过验证的算法可以提取代码，实验表明提取的代码表现出了合理的效率。
Ordinary differential equations (ODEs) are ubiquitous when modeling continuous dynamics. Classical numerical methods compute approximations of the solution, however without any guarantees on the quality of the approximation. Nevertheless, methods have been developed that are supposed to compute enclosures of the solution.In this paper, we demonstrate that enclosures of the solution can be verified with a high level of rigor: We implement a functional algorithm that computes enclosures of solutions of ODEs in the interactive theorem prover Isabelle/HOL, where we formally verify (and have mechanically checked) the safety of the enclosures against the existing theory of ODEs in Isabelle/HOL.Our algorithm works with dyadic rational numbers with statically fixed precision and is based on the well-known Euler method. We abstract discretization and round-off errors in the domain of affine forms. Code can be extracted from the verified algorithm and experiments indicate that the extracted code exhibits reasonable efficiency.
登录
查看更多内容
影响因子：
1.2
作者：
Steven Obua;T. Nipkow
通讯作者：
Steven Obua;T. Nipkow
简单算术和代数形式化证明的自动化方法（Automatische Methoden für formale Beweise in einfachen Arithmetiken und Algebren）
DOI：
--
发表时间：
2008
期刊：
影响因子：
--
作者：
A. Chaieb
通讯作者：
A. Chaieb
DOI：
10.17863/cam.23640
发表时间：
2000-10
期刊：
ArXiv
影响因子：
--
作者：
Lawrence Charles Paulson
通讯作者：
Lawrence Charles Paulson
IEEE浮点运算的形式化模型
DOI：
--
发表时间：
2013
期刊：
Arch. Formal Proofs
影响因子：
--
作者：
Lei Yu
通讯作者：
Lei Yu
Einschliessung der Lösung gewöhnlicher Anfangs- und Randwertaufgaben und Anwendungen
DOI：
--
发表时间：
1988
期刊：
影响因子：
--
作者：
R. Lohner
通讯作者：
R. Lohner