Email Gateway (Aug 18 2022 at 17:50): Email Gateway (Aug 18 2022 at 17:50):From: Tjark Weber <webertj@in.tum.de>
I am pleased to announce two related papers that describe an
Isabelle/HOL repository of algebraic structures:
[1] Automating Algebraic Methods in Isabelle (ICFEM 2011, joint work
with Walter Guttmann and Georg Struth)
Abstract (provisional):
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 many popular 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 and concise.
This is a step towards increasing the automation of formal methods.
[2] Automated Engineering of Relational and Algebraic Methods in
Isabelle/HOL - Invited Tutorial (RAMICS 2011, joint work with Simon
Foster and Georg Struth)
Kind regards,
Tjark
Last updated: Apr 26 2024 at 20:16 UTC