Tutorial on The Isabelle Refinement Framework and Autoref
About the Refinement Framework
The Isabelle Refinement and Autoref Frameworks support a stepwise refinement approach to verified program development, using the theorem prover Isabelle/HOL. It can be used to produce verified, efficiently executable algorithms. It is accompanied by the Isabelle Collection Framework, which provides an extensive library of reusable verified functional data structures.
Here are some examples for algorithms and software systems that use the Refinement Framework:
- The CAVA model checker (See also our CAV-13 Paper)
- Gabow's SCC algorithm (See also our ITP-14 Paper)
- Dijkstra's shortest paths algorithm
- Hopcroft's automata minimization algorithm (Described in our ITP-12 Paper)
While this tutorial covers refinement to purely functional programs only, the Sepref-Tool also supports refinement to imperative programs. The above link also contains a userguide, which may be a good follow-up to this tutorial / an alternative to the Autoref-part of this tutorial.
About this Tutorial
This tutorial covers the basics of the refinement framework and the Autoref tool. It is a combination of some theoretical background, tool demo, and do-it-yourself parts. It can be given in roughly two days.
It requires a solid knowledge of Isabelle, and a bit of background in Hoare logic and programming with monads.
Material
Note:The theories require Isabelle 2016-1 with the AFP component installed.
refine_tutorial.tgz
run isabelle.sh to start the IDE. On first invocation, it will build the image, which will take some time.
Slides: refine_slides.pdf
Old Isabelle 2016 version: refine_tutorial_old_2016.tgz
Old Isabelle 2014 version: refine_tutorial_old.tgz