Algebraic verification of hybrid systems in Isabelle/HOL

The thesis describes an open modular semantic framework for the verification of hybrid systems in a general-purpose proof assistant. We follow this approach to create the first algebraic based verification components for hybrid systems in Isabelle/HOL. The framework benefits from various design choices. Firstly, an algebra for programs such as Kleene algebras with tests or modal Kleene algebras captures the verification condition generation by providing rules for each programming construct. Intermediate relational or state transformer semantics instantiated to a concrete model of the program store allow the framework to handle assignments and ordinary differential equations (ODEs). The verification rules for ODEs require user-provided solutions, differential invariants or analytical descriptions of the continuous dynamics of the system. The construction is a shallow embedding which makes the approach quickly extensible and modular. Taking advantage of these features, we derive differential Hoare logic (dH), a minimalistic logic for the verification of hybrid systems, and the differential refinement calculus (dR) for their stepwise construction. Yet the approach is not limited to these formalisms. We also present a hybrid weakest liberal precondition calculus based on predicate transformers which subsumes powerful deductive verification approaches like differential dynamic logic. The framework is also compositional: we combine it with lenses to vary the model of the program store. We also support it with a formalisation of affine and linear systems of ordinary differential equations in Isabelle/HOL. This integration simplifies various certifications that the proof assistant requires such as guarantees of existence and uniqueness of the corresponding solutions. Verification examples illustrate the approach at work. Formalisations of our solutions to problems of the international friendly competition ARCH2020, where our components participated, further evidence their effectiveness. Finally, a larger case study certifying an invariant for a PID controller of the roll angle in a quadcopter’s flight complements these verifications.