| Automated Machine-Checked Hybrid System Safety Proofs |  |
Abstract:
We have developed a hybrid system safety prover, implemented in Coq using the abstraction method introduced by Alur, Dang
and Ivancic (2006). The development includes: a formalisation of the structure of hybrid systems; a framework for the
construction of an abstract system (consisting of decidable "over-estimators" of abstract transitions and initiality)
faithfully representing a concrete hybrid system; a translation of abstract systems to graphs, enabling the decision of
abstract state reachability using a certified graph reachability algorithm; a proof of the safety of an example hybrid
system generated using this tool stack. To produce fully certified safety proofs without relying on floating point
computations, the development critically relies on the computable real number implementation of the CoRN library of
constructive mathematics formalised in Coq. The development also features a nice interplay between constructive and
classical logic via the double negation monad.
Automated Machine-Checked Hybrid System Safety Proofs
In
Proceedings of the International Conference on Interactive Theorem Proving
( ITP '10),
Edinburgh, Scotland.
BibTeX:@inproceedings{hybrid-ITP-10,
author = {Herman Geuvers and Adam Koprowski and Dan Synek and Eelis van der Weegen},
title = {Automated Machine-Checked Hybrid System Safety Proofs},
booktitle = {Proceedings of the International Conference on Interactive Theorem Proving (ITP '10)},
year = {2010},
series = {Lecture Notes in Computer Science},
volume = {6172},
pages = {259--274},
} | 
