@inproceedings{imm-15-aa-reach,
  author = {Fabian Immler},
  title = {Verified Reachability Analysis of Continuous Systems},
  booktitle = {Proc 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015)},
  series = {LNCS},
  volume = {9035},
  pages = {37–51},
  doi = {10.1007/978-3-662-46681-0_3},
  publisher = {Springer},
  year = 2015,
  month = apr,
  comment = {Solution of ODEs},
  abstract = {Ordinary differential equations (ODEs) are often used to model the dynamics of (often safety-critical) continuous systems. This work presents the formal verification of an algorithm for reachability analysis in continuous systems. The algorithm features adaptive Runge-Kutta methods and rigorous numerics based on affine arithmetic. It is proved to be sound with respect to the existing formalization of ODEs in Isabelle/HOL. Optimizations like splitting, intersecting and collecting reachable sets are necessary to analyze chaotic systems. Experiments demonstrate the practical usability of our developments.}
}