Alasdair Armstrong, Georg Struth, and Tjark Weber. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science, pages 197-212. Springer, 2013.
Schematic Kleene algebra with tests (SKAT) supports the equational verification of flowchart scheme equivalence and captures simple while-programs with assignment statements. We formalise SKAT in Isabelle/HOL, using the quotient type package to reason equationally in this algebra. We apply this formalisation to a complex flowchart transformation proof from the literature. We extend SKAT with assertion statements and derive the inference rules of Hoare logic. We apply this extension in simple program verification examples and the derivation of additional Hoare-style rules. This shows that algebra can provide an abstract semantic layer from which different program analysis and verification tasks can be implemented in a simple lightweight way.
The original publication is available at www.springerlink.com.
@inproceedings{armstrong13program,
author = {Alasdair Armstrong and Georg Struth and Tjark Weber},
title = {Program Analysis and Verification Based on {Kleene} Algebra in {Isabelle/HOL}},
editor = {Sandrine Blazy and Christine Paulin-Mohring and David Pichardie},
booktitle = {Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July~22-26, 2013. Proceedings},
volume = {7998},
series = {Lecture Notes in Computer Science},
pages = {197--212},
publisher = {Springer},
year = {2013},
url = {http://dx.doi.org/10.1007/978-3-642-39634-2_16}
}