[Club2] Talk by Fabian Immler -- Wed., Apr. 16, 15:00, Room: Turing (00.09.38)

[Andrei Popescu]

Dear All,  

Tomorrow, Fabian will give a talk on his work on certified algorithms 
for approximating solutions of differential equations. This is a rehearsal 
for his NASA Formal Methods Symposium presentation.    
 
Cheers, 
  Andrei  


Formally Verified Computation of Enclosures of Solutions of Ordinary
Differential Equations
Fabian Immler
======================================================================
Wed., Apr. 16, 15:00, Room: Turing (00.09.38)

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20140415/c4f788f1/attachment.html>