adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof/drefine
History
Matthew Brecknell 7d0425dd3e Isabelle2016-1: fix proofs using lemmas now removed 
Some lemmas that were specific instances of more general lemmas have
been removed from the library. In most cases, broken references could
simply be replaced with the more general fact.
 		2017-01-05 14:23:11 +11:00
..
Arch_DR.thy Isabelle2016-1: update references to renamed constants and facts 2017-01-05 14:23:05 +11:00
CNode_DR.thy Isabelle2016-1: update references to renamed constants and facts 2017-01-05 14:23:05 +11:00
Corres_D.thy SELFOUR-276: Finish proofs for maximum controlled priority (MCP) 2016-10-05 02:43:41 +11:00
Finalise_DR.thy Isabelle2016-1: update references to renamed constants and facts 2017-01-05 14:23:05 +11:00
Include_D.thy comment cleanup 2014-07-22 18:10:20 +02:00
Intent_DR.thy Isabelle2016-1: update references to renamed constants and facts 2017-01-05 14:23:05 +11:00
Interrupt_DR.thy Updating remaining proofs for tcb_arch reserved_irq and arch_fault changes 2016-11-25 13:51:07 +11:00
Ipc_DR.thy Isabelle2016-1: update references to renamed constants and facts 2017-01-05 14:23:05 +11:00
KHeap_DR.thy Isabelle2016-1: fix proofs using lemmas now removed 2017-01-05 14:23:11 +11:00
Lemmas_D.thy Some more cleanup of drefine. 2014-07-23 15:29:20 +10:00
MoreCorres.thy Fix DRefine to accommodate corres_underlying changes. 2016-05-13 12:05:53 +10:00
MoreHOL.thy Import release snapshot. 2014-07-14 21:32:44 +02:00
README.md misc: Proofing and formatting of README.md files. 2014-07-28 13:15:48 +10:00
Refine_D.thy ADT: add kernel entry/exit constraints on domain time left 2016-11-11 06:01:30 +11:00
Schedule_DR.thy Isabelle2016-1: update references to renamed constants and facts 2017-01-05 14:23:05 +11:00
StateTranslationProofs_DR.thy Isabelle2016-1: update references to renamed constants and facts 2017-01-05 14:23:05 +11:00
StateTranslation_D.thy Isabelle2016-1: update references to renamed constants and facts 2017-01-05 14:23:05 +11:00
Syscall_DR.thy Isabelle2016-1: update references to renamed constants and facts 2017-01-05 14:23:05 +11:00
Tcb_DR.thy Isabelle2016-1: update references to renamed constants and facts 2017-01-05 14:23:05 +11:00
Untyped_DR.thy Isabelle2016-1: update references to renamed constants and facts 2017-01-05 14:23:05 +11:00

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 from the l4v/ directory, run:

./isabelle/bin/isabelle build -d . -v -b 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.