e9180d5cb5
|
||
|---|---|---|
| .. | ||
| ADT_H.thy | ||
| ArchAcc_R.thy | ||
| Arch_R.thy | ||
| Bits_R.thy | ||
| BuildRefineCache.thy | ||
| CNodeInv_R.thy | ||
| CSpace1_R.thy | ||
| CSpace_I.thy | ||
| CSpace_R.thy | ||
| Cache.thy | ||
| Corres.thy | ||
| Detype_R.thy | ||
| EmptyFail.thy | ||
| EmptyFail_H.thy | ||
| Finalise_R.thy | ||
| IncKernelInit.thy | ||
| Include.thy | ||
| InitLemmas.thy | ||
| InterruptAcc_R.thy | ||
| Interrupt_R.thy | ||
| Invariants_H.thy | ||
| Invocations_R.thy | ||
| IpcCancel_R.thy | ||
| Ipc_R.thy | ||
| KHeap_R.thy | ||
| KernelInit_R.thy | ||
| LevityCatch.thy | ||
| Machine_R.thy | ||
| Orphanage.thy | ||
| PageTableDuplicates.thy | ||
| README.md | ||
| Refine.thy | ||
| Retype_R.thy | ||
| Schedule_R.thy | ||
| StateRelation.thy | ||
| SubMonad_R.thy | ||
| Syscall_R.thy | ||
| TcbAcc_R.thy | ||
| Tcb_R.thy | ||
| Untyped_R.thy | ||
| VSpace_R.thy | ||
README.md
Design Spec Refinement Proof
This proof establishes that seL4's design specification is a formal refinement (i.e. a correct implementation) of its abstract specification. This proof also interweaves the definition and proofs of the global invariant for the design specification, and builds on the Abstract Spec Invariant Proof. It is described in the TPHOLS '08 paper.
Building
To build from the l4v/ directory, run:
./isabelle/bin/isabelle build -d . -v -b Refine
Important Theories
The top-level theory where the refinement statement is established over
the entire kernel is Refine; the state-relation that
relates the state-spaces of the two specifications is defined in
StateRelation and the basic correspondence
property proved over each kernel function is defined in
Corres.