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