Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better\n Models, Faster Proofs

We extend a semantic verification framework for hybrid systems with the\nIsabelle/HOL proof assistant by an algebraic model for hybrid program stores, a\nshallow expression model for hybrid programs and their correctness\nspecifications, and domain-specific deductive and calculational support. The\nnew store model yields clean separations and dynamic local views of variables,\ne.g. discrete/continuous, mutable/immutable, program/logical, and enhanced ways\nof manipulating them using combinators, projections and framing. This leads to\nmore local inference rules, procedures and tactics for reasoning with invariant\nsets, certifying solutions of hybrid specifications or calculating derivatives\nwith increased proof automation and scalability. The new expression model\nprovides more user-friendly syntax, better control of name spaces and\ninterfaces connecting the framework with real-world modelling languages.\n