Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification

摘要

We formalise mathematical components for solving affine and linear systems of ordinary differential equations in Isabelle/HOL. The formalisation integrates the theory stacks of linear algebra and analysis and substantially adds content to both of them. It also serves to improve extant verification components for hybrid systems by increasing proof automation, removing certification procedures, and decreasing the number of proof obligations. We showcase these advantages through examples.