Building Verification Tools with Isabelle
This course shows how program verification tools can be prototyped
quickly and easily from suitable algebras for the control flow with
the interactive theorem prover Isabelle/HOL. The course is split into
four parts. The first one introduces variants of Kleene algebras and
quantales as control flow algebras. The second on provides a brief
introduction to Isabelle/HOL. The third part shows the implementation
of a simple tool for the construction and verification of simple
while-programs. The fourth part discusses extensions of this approach
to separation logic and concurrency verification based on the
rely-guarantee method.
Last modified: Thu Apr 9 12:21:21 BST 2015