Walter Guttmann, Georg Struth, and Tjark Weber. In Shengchao Qin and Zongyan Qiu, editors, Formal Methods and Software Engineering - 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011. Proceedings, volume 6991 of Lecture Notes in Computer Science, pages 617-632. Springer, 2011.
We implement a large Isabelle/HOL repository of algebras for application in modelling computing systems. They subsume computational logics such as dynamic and Hoare logics and form a basis for various software development methods. Isabelle has recently been extended by automated theorem provers and SMT solvers.We use these integrated tools for automatically proving several rather intricate refinement and termination theorems. We also automate a modal correspondence result and soundness and relative completeness proofs of propositional Hoare logic. These results show, for the first time, that Isabelle's tool integration makes automated algebraic reasoning particularly simple. This is a step towards increasing the automation of formal methods.
The original publication is available at www.springerlink.com.
@inproceedings{guttmann11automating,
author = {Walter Guttmann and Georg Struth and Tjark Weber},
title = {Automating Algebraic Methods in {Isabelle}},
editor = {Shengchao Qin and Zongyan Qiu},
booktitle = {Formal Methods and Software Engineering - 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October~26-28, 2011. Proceedings},
volume = {6991},
series = {Lecture Notes in Computer Science},
pages = {617--632},
publisher = {Springer},
url = {http://dx.doi.org/10.1007/978-3-642-24559-6_41},
year = {2011}
}