Modal Kleene algebras have been used for building verification components for imperative programs with Isabelle/HOL. We integrate this approach with recent Isabelle components for ordinary differ-ential equations to build two verification components for hybrid systems, where continuous phase space dynamics complement the discrete dynamics on program stores. We demonstrate their feasibility by deriving the most important domain-specific rules of differential dynamic logic and discussing four simple examples.
展开▼
