README.md
1CapDL Refinement Proof
2======================
3
4This proof establishes that seL4's [abstract specification][aspec] is
5a formal *refinement* (i.e. a correct implementation) of its [capDL
6specification][capDL]. It is described as part of an ICFEM '13
7[paper][paper].
8
9 [aspec]: ../../spec/abstract/
10 [capdl]: ../../spec/capDL/
11 [paper]: http://www.nicta.com.au/pub?id=7047 "Formally Verified System Initialisation"
12
13Building
14--------
15
16To build from the `l4v/` directory, run:
17
18 ./isabelle/bin/isabelle build -d . -v -b DRefine
19
20Important Theories
21------------------
22
23The top-level theory where the refinement statement is established over
24the entire kernel is [`Refine_D`](Refine_D.thy); the state-relation that
25relates the state-spaces of the two specifications is defined in
26[`StateTranslation_D`](StateTranslation_D.thy) and the basic
27correspondence property proved over each kernel function is defined in
28[`Corres_D`](Corres_D.thy).
29
30