NameDateSize

..25-Jul-201916

Arch_DR.thyH A D25-Jul-201996.4 KiB

CNode_DR.thyH A D25-Jul-2019131.7 KiB

Corres_D.thyH A D25-Jul-201927.8 KiB

Finalise_DR.thyH A D25-Jul-2019173.5 KiB

Include_D.thyH A D25-Jul-2019493

Intent_DR.thyH A D25-Jul-201996.6 KiB

Interrupt_DR.thyH A D25-Jul-201929.4 KiB

Ipc_DR.thyH A D25-Jul-2019134.5 KiB

KHeap_DR.thyH A D25-Jul-2019166.5 KiB

Lemmas_D.thyH A D25-Jul-20191.1 KiB

MoreCorres.thyH A D25-Jul-20194.8 KiB

MoreHOL.thyH A D25-Jul-2019494

README.mdH A D25-Jul-2019941

Refine_D.thyH A D25-Jul-20192.5 KiB

Schedule_DR.thyH A D25-Jul-201935.7 KiB

StateTranslation_D.thyH A D25-Jul-201946.9 KiB

StateTranslationProofs_DR.thyH A D25-Jul-201912.9 KiB

Syscall_DR.thyH A D25-Jul-201981.9 KiB

Tcb_DR.thyH A D25-Jul-201988.7 KiB

Untyped_DR.thyH A D25-Jul-201986.9 KiB

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