mirror of https://github.com/seL4/l4v.git
a690fd7288
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems> |
||
|---|---|---|
| .. | ||
| base | ||
| Arch_DR.thy | ||
| CNode_DR.thy | ||
| Corres_D.thy | ||
| Finalise_DR.thy | ||
| Intent_DR.thy | ||
| Interrupt_DR.thy | ||
| Ipc_DR.thy | ||
| KHeap_DR.thy | ||
| Lemmas_D.thy | ||
| MoreCorres.thy | ||
| MoreHOL.thy | ||
| README.md | ||
| Refine_D.thy | ||
| Schedule_DR.thy | ||
| StateTranslationProofs_DR.thy | ||
| StateTranslation_D.thy | ||
| Syscall_DR.thy | ||
| Tcb_DR.thy | ||
| Untyped_DR.thy | ||
README.md
CapDL Refinement Proof
This proof establishes that seL4's abstract specification is a formal refinement (i.e. a correct implementation) of its capDL specification. It is described as part of an ICFEM '13 paper.
Building
To build for the ARM architecture from the l4v/ directory, run:
L4V_ARCH=ARM ./run_tests DRefine
Important Theories
The top-level theory where the refinement statement is established over
the entire kernel is Refine_D; the state-relation that
relates the state-spaces of the two specifications is defined in
StateTranslation_D and the basic
correspondence property proved over each kernel function is defined in
Corres_D.