Advertisement
Published in:
2011 | OriginalPaper | Chapter
Automating Algebraic Methods in Isabelle
Authors : Walter Guttmann, Georg Struth, Tjark Weber
Published in: Formal Methods and Software Engineering
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.