Download the Graph Refinement toolset
What am I downloading?
You are downloading the NICTA graph refinement toolset.
The toolset consists of a python program and a collection of Isabelle/HOL theories used to reason about programs in a particular graph representation. These tools were first used to demonstrate that binary images of seL4 are refinements of the C models produced by the NICTA C parser as part of the NICTA compilation correctness project.
The design and proof rules of the graph refinement toolset are described in detail in the paper "Translation Validation for a Verified OS Kernel", see below.
The initial release of the graph-refinenement toolset includes the core graph refinement program but only a subset of the Isabelle theories used in the compilation correctness project. Further theories that were used to convert the Isabelle/SIMPL representation of seL4 into an input problem for graph refinement will be provided in a future release.
The graph refinement tools are released under the BSD license. The tar file for download bundles the NICTA C parser, also under the BSD license, which in turn bundles the following 3rd party components:
- the language Simpl by Norbert Schirmer under the LGPL license
- code from SML/NJ under a BSD-style license
- code from the mlton compiler under a BSD-style license
The python graph refinement program requires the use of an SMT solver, which is not included. We have had success using the solvers Z3 (version 4.0) and SONOLAR (version 2012-06-14), but other SMTLIB2 compatible solvers may be effective. The list of available solvers should be adjusted in the file "solver.py".
The Isabelle theories included require the use of Isabelle 2012, and may be built conveniently from the HOL-Word image.
- graph-refine-0.1.tgz (Released 18 Jul, 2013, Isabelle 2012)
||Thomas Sewell, Magnus Myreen and Gerwin Klein|
Translation validation for a verified OS kernel
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471–481, Seattle, Washington, USA, June, 2013