Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Berz, M., Makino, K.: Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliable Computing 4(4), 361–369 (1998)
Boldo, S., Clément, F., Filliâtre, J.C., Mayero, M., Melquiond, G., Weis, P.: Wave equation numerical resolution: A comprehensive mechanized proof of a C program. Journal of Automated Reasoning 50(4), 423–456 (2012)
Bouissou, O., Chapoutot, A., Djoudi, A.: Enclosing temporal evolution of dynamical systems using numerical methods. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 108–123. Springer, Heidelberg (2013)
Brisebarre, N., Joldeş, M., Martin-Dorel, É., Mayero, M., Muller, J.-M., Paşca, I., Rideau, L., Théry, L.: Rigorous Polynomial Approximation Using Taylor Models in Coq. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 85–99. Springer, Heidelberg (2012)
Chaieb, A.: Automated methods for formal proofs in simple arithmetic and algebra. Diss., Technische Universität, München (2008)
de Figueiredo, L.H., Stolfi, J.: Affine Arithmetic: Concepts and Applications. Numerical Algorithms 37(1-4), 147–158 (2004)
Haftmann, F., Krauss, A., Kunčar, O., Nipkow, T.: Data refinement in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 100–115. Springer, Heidelberg (2013)
Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103–117. Springer, Heidelberg (2010)
Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 114–129. Springer, Heidelberg (2005)
Hölzl, J.: Proving inequalities over reals with computation in Isabelle/HOL. In: Reis, G.D., Théry, L. (eds.) Programming Languages for Mechanized Mathematics Systems (ACM SIGSAM 2009), pp. 38–45 (2009)
Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 279–294. Springer, Heidelberg (2013)
Immler, F.: Affine Arithmetic. Archive of Formal Proofs (February 2014), http://afp.sf.net/devel-entries/Affine_Arithmetic.shtml
Immler, F., Hölzl, J.: Numerical Analysis of Ordinary Differential Equations in Isabelle / HOL. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 377–392. Springer, Heidelberg (2012)
Immler, F., Hölzl, J.: Ordinary differential equations. Archive of Formal Proofs (February 2014), http://afp.sf.net/devel-entries/Ordinary_Differential_Equations.shtml
Lohner, R.: Einschliessung der Lösung gewöhnlicher Anfangs- und Randwertaufgaben und Anwendungen. Dissertation, Universität Karlsruhe (1988)
Makarov, E., Spitters, B.: The Picard algorithm for ordinary differential equations in Coq. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 463–468. Springer, Heidelberg (2013)
Nedialkov, N.S., Jackson, K.R.: The design and implementation of a validated object-oriented solver for IVPs for ODEs. Tech. rep., McMaster University (2002)
Nedialkov, N.S.: Interval tools for ODEs and DAEs. In: 12th GAMM-IMACS International Symposium SCAN. IEEE (2006)
Nedialkov, N.S.: Implementing a rigorous ODE solver through literate programming. In: Rauh, A., Auer, E. (eds.) Modeling, Design, and Simulation of Systems with Uncertainties. Mathematical Engineering, pp. 3–19. Springer (2011)
Neher, M., Jackson, K.R., Nedialkov, N.S.: On Taylor model based integration of ODEs. SIAM Journal on Numerical Analysis 45(1), 236–262 (2007)
Obua, S.: Flyspeck II: The basic linear programs. Diss., Technische Universität München, München (2008)
Paulson, L.C.: Isabelle: The next 700 theorem provers. In: Logic and Computer Science, pp. 361–386 (1990)
Platzer, A.: The complete proof theory of hybrid system. In: Logic in Computer Science (LICS), pp. 541–550 (2012)
Revol, N., Makino, K., Berz, M.: Taylor models and floating-point arithmetic: Proof that arithmetic operations are validated in COSY. The Journal of Logic and Algebraic Programming 64(1), 135–154 (2005)
Stauning, O.: Automatic validation of numerical solutions. Diss., Technical University of Denmark (1997)
Tucker, W.: A rigorous ODE solver and Smale’s 14th problem. Foundations of Computational Mathematics 2(1), 53–117 (2002)
Yu, L.: A Formal Model of IEEE Floating Point Arithmetic. Archive of Formal Proofs (2013), http://afp.sf.net/entries/IEEE_Floating_Point.shtml
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Immler, F. (2014). Formally Verified Computation of Enclosures of Solutions of Ordinary Differential Equations. In: Badger, J.M., Rozier, K.Y. (eds) NASA Formal Methods. NFM 2014. Lecture Notes in Computer Science, vol 8430. Springer, Cham. https://doi.org/10.1007/978-3-319-06200-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-06200-6_9
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06199-3
Online ISBN: 978-3-319-06200-6
eBook Packages: Computer ScienceComputer Science (R0)