Skip to main content
SpringerLink
Log in
Book cover

Modeling, Design, and Simulation of Systems with Uncertainties pp 3–19Cite as

Implementing a Rigorous ODE Solver Through Literate Programming

  • Chapter
  • First Online:

Part of the book series: Mathematical Engineering ((MATHENGIN,volume 3))

Abstract

Interval numerical methods produce results that can have the power of a mathematical proof. Although there is a substantial amount of theoretical work on these methods, little has been done to ensure that an implementation of an interval method can be readily verified. However, when claiming rigorous numerical results, it is crucial to ensure that there are no errors in their computation. Furthermore, when such a method is used in a computer assisted proof, it would be desirable to have its implementation published in a form that is convenient for verification by human experts. We have applied Literate Programming (LP) to produce VNODE-LP, a C++ solver for computing rigorous bounds on the solution of an initial-value problem (IVP) for an ordinary differential equation (ODE).We have found LP well suited for ensuring that an implementation of a numerical algorithm is a correct translation of its underlying theory into a programming language: we can split the theory into small pieces, translate each of them, and keep mathematical expressions and the corresponding code close together in a unified document. Then it can be reviewed and checked for correctness by human experts, similarly to how a scientific work is examined in a peer-review process.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Achlioptas, D.: Setting 2 variables at a time yields a new lower bound for random 3-SAT. Tech. Rep. MSR-TR-99-96, Microsoft Research, Microsoft Corp., One Microsoft Way, Redmond, WA 98052 (1999)

    Google Scholar 

  2. Auer, E., Kecskem´ethy, A., T¨andl, M., Traczinski, H.: Interval algorithms in modelling of multibody systems. In: Numerical Software with Result Verification, LNCS, vol. 2991, pp. 132–159. Springer-Verlag (2004)

    Google Scholar 

  3. Berz, M.: COSY INFINITY version 8 reference manual. Technical Report MSUCL–1088, National Superconducting Cyclotron Lab., Michigan State University, East Lansing, Mich. (1997)

    Google Scholar 

  4. Brown, B.M., Langer, M., Marletta, M., Tretter, C., Wagenhofer, M.: Eigenvalue bounds for the singular Sturm-Liouville problem with a complex potential. J. Phys. A:Math. Gen. 36(13), 3773–3787 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  5. Dietrich, S.: Adaptive verifizierte l¨osung gew¨ohnlicher differentialgleichungen. Ph.D. thesis, University of Karlsruhe, Karlsruhe, Germany (2003)

    Google Scholar 

  6. Goualard, F.: Gaol: Not just another interval library (version 2.0.2). http://sourceforge.net/projects/gaol/ (2006)

    Google Scholar 

  7. Hayes, W.: Rigorous shadowing of numerical solutions of ordinary differential equations by containment. Ph.D. thesis, Department of Computer Science, University of Toronto, Toronto, Canada (2001)

    Google Scholar 

  8. Hayes, W., Jackson, K.R.: Rigorous shadowing of numerical solutions of ordinary differential equations by containment. SIAM J. Numer. Anal. 42(5), 1948–1973 (2003)

    Article  MathSciNet  Google Scholar 

  9. Ishii, D.: Simulation and verification of hybrid systems based on interval analysis and constraint programming. Ph.D. thesis, Graduate School of Science and Engineering, Waseda University, Japan (2010)

    Google Scholar 

  10. Jackson, K.R., Nedialkov, N.S.: Some recent advances in validated methods for IVPs for ODEs. Appl. Numer. Math. 42, 269–284 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  11. Johnson, A., Johnson, B.: Literate programming using noweb. Linux J., Article No 1 (1997)

    Google Scholar 

  12. Kieffer, M., Walter, E.: Nonlinear parameter and state estimation for cooperative systems in a bounded-error context. In: Numerical Software with Result Verification, LNCS, vol. 2991, pp. 107–123. Springer-Verlag (2004)

    Google Scholar 

  13. Kn¨uppel, O.: PROFIL/BIAS – a fast interval library. Computing 53(3–4), 277–287 (1994)

    Google Scholar 

  14. Knuth, D.E.: The WEB system of structured documentation. Stanford Computer Science Report CS980, Stanford University, Stanford, CA (1983)

    Google Scholar 

  15. Knuth, D.E.: Literate programming. Technical report STAN-CS-83-981, Stanford University, Department of Computer Science (1983)

    Google Scholar 

  16. Knuth, D.E.: Literate Programming. Center for the Study of Language and Information, Stanford, CA, USA (1992)

    MATH  Google Scholar 

  17. Knuth, D.E., Levy, S.: The CWEB System of Structured Documentation. Addison-Wesley, Reading, Massachusetts (1993)

    Google Scholar 

  18. Lee, C.K.: Robust evaluation of differential geometry properties using interval arithmetic techniques. Master’s thesis, Massachusetts Institute of Technology, Department of Ocean Engineering (2005)

    Google Scholar 

  19. Lerch, M., Tischler, G., Gudenberg, J.W.V., Hofschuster, W., Kr¨amer, W.: FILIB++, a fast interval library supporting containment computations. ACM Trans. Math. Softw. 32(2), 299–324 (2006)

    Google Scholar 

  20. Lin, Y., Stadtherr, M.A.: Validated solution of initial value problems for ODEs with interval parameters. In: R.L. Muhanna, R.L. Mullen (eds.) Proceedings of 2nd NSF Workshop on Reliable Engineering Computing. Savannah, GA (2006)

    Google Scholar 

  21. Literate programming web site. http://www.literateprogramming.com

    Google Scholar 

  22. Lohner, R.J.: Einschließung der L¨osung gew¨ohnlicher Anfangs– und Randwertaufgaben und Anwendungen. Ph.D. thesis, Universit¨at Karlsruhe (1988)

    Google Scholar 

  23. Moore, A.P., Payne, C.N., Jr.: Increasing assurance with literate programming techniques. In: Proceedings of 11th Annual Conference on Computer Assurance. COMPASS ’96, pp. 187–198 (1996)

    Google Scholar 

  24. Mukundan, H., Ko, K.H., Maekawa, T., Sakkalis, T., Patrikalakis, N.M.: Tracing surface intersections with a validated ODE system solver. In: G. Elber, G. Taubin (eds.) Proceedings of the Ninth EG/ACM Symposium on Solid Modeling and Applications. Eurographics Press, June 2004 (2004)

    Google Scholar 

  25. Nedialkov, N.S.: Computing rigorous bounds on the solution of an initial value problem for an ordinary differential equation. Ph.D. thesis, Department of Computer Science, University of Toronto, Toronto, Canada, M5S 3G4 (1999)

    Google Scholar 

  26. Nedialkov, N.S.: Interval tools for ODEs and DAEs. In: SCAN Conference Proceedings, http://www.computer.org/portal/web/csdl/doi/10.1109/SCAN.2006. 28 (2006)

    Google Scholar 

  27. Nedialkov, N.S.: VNODE-LP — a validated solver for initial value problems in ordinary differential equations. Tech. Rep. CAS-06-06-NN, Department of Computing and Software, McMaster University, Hamilton, Canada, L8S 4K1 (2006). VNODE-LP is available at http://www.cas.mcmaster.ca/˜nedialk/vnodelp

    Google Scholar 

  28. Nedialkov, N.S., Jackson, K.R.: The design and implementation of a validated object-oriented solver for IVPs for ODEs. Tech. Rep. 6, Software Quality Research Laboratory, Department of Computing and Software, McMaster University, Hamilton, Canada, L8S 4K1 (2002)

    Google Scholar 

  29. Nedialkov, N.S., Jackson, K.R., Corliss, G.F.: Validated solutions of initial value problems for ordinary differential equations. Appl. Math. Comp. 105(1), 21–68 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  30. Neumaier, A.: Interval Methods for Systems of Equations. Cambridge University Press, Cambridge (1990)

    MATH  Google Scholar 

  31. Parnas, D.L.: Inspection of safety-critical software using program-function tables. In: Software fundamentals: collected papers by David L. Parnas, pp. 371–382. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA (2001)

    Google Scholar 

  32. Patrikalakis, N.M.,Maekawa, T., Ko, K.H.,Mukundan, H.: Surface to surface intersection. In: L. Piegl (ed.) International CAD Conference and Exhibition, CAD’04. Thailand (2004)

    Google Scholar 

  33. Pharr, M., Humphreys, G.: Physically Based Rendering: From Theory to Implementation. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (2004)

    Google Scholar 

  34. Ramdani, N., Meslem, N., Ra¨ıssi, T., Candau, Y.: Set-membership identification of continuous-time systems. In: B. Ninness, H. Hjalmarsson (eds.) 14th IFAC Symposium on System Identification, 2006, vol. 14. IFAC (2007)

    Google Scholar 

  35. Rump, S.: Verification methods: Rigorous results using floating-point arithmetic. In: Acta Numerica, pp. 287–449. Cambridge University Press (2010)

    Google Scholar 

  36. Schrod, J.: The cweb class. CTAN, the Comprehensive TEX Archive Network (1995)

    Google Scholar 

  37. Schrod, J.: Typesetting cweave output. CTAN, the Comprehensive TEX Archive Network (1995)

    Google Scholar 

  38. Smith, L.M.C., Samadzadeh, M.H.: An annotated bibliography of literate programming. ACM SIGPLAN Notices 26(1), 14–20 (1991)

    Article  Google Scholar 

  39. Stauning, O.: Automatic validation of numerical solutions. Ph.D. thesis, Technical University of Denmark, DK-2800, Lyngby, Denmark (1997)

    Google Scholar 

  40. Stauning, O., Bendtsen, C.: FADBAD++ web page (2003). http://www.imm.dtu.dk/fadbad.html

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada, L8S 4K1

    Nedialko S. Nedialkov

Authors
  1. Nedialko S. Nedialkov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nedialko S. Nedialkov .

Editor information

Editors and Affiliations

  1. , Chair of Mechatronics, University of Rostock, Justus-von-Liebig-Str. 6, Rostock, 18059, Germany

    Andreas Rauh

  2. , Faculty of Engineering, INKO, University of Duisburg-Essen, Duisburg, 47048, Germany

    Ekaterina Auer

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Nedialkov, N.S. (2011). Implementing a Rigorous ODE Solver Through Literate Programming. In: Rauh, A., Auer, E. (eds) Modeling, Design, and Simulation of Systems with Uncertainties. Mathematical Engineering, vol 3. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15956-5_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15956-5_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15955-8

  • Online ISBN: 978-3-642-15956-5

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation