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 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.
|
 |
Gernot Heiser, Gerwin Klein and June Andronick seL4 in Australia: From research to real-world trustworthy systems Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020 |
|
|
|
Thomas Sewell Translation validation for verified, efficient and timely operating systems PhD Thesis, UNSW, Sydney, Australia, 2017 |
|
|
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 |