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.
Author supplied keywords
Cite
CITATION STYLE
Immler, F. (2015). Verified reachability analysis of continuous systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9035, pp. 37–51). Springer Verlag. https://doi.org/10.1007/978-3-662-46681-0_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
