Mario Gleirscher

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

2021 · arXiv (Cornell University)

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 …