adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Gerwin Klein 57bef16d8e sync Makefile and test.xml 2014-11-23 19:54:59 +11:00
..
access-control de-bitrot DPolicy; add back into regression 2014-11-23 14:52:21 +11:00
asmrefine Don't reuse the s_footprint_intvl theorem name. 2014-10-01 11:16:40 +10:00
bisim bisim: Isabelle 2014 changes. 2014-09-24 12:24:00 +10:00
capDL-api Merge branch 'master' into 'isabelle-2014'. 2014-09-23 14:31:33 +10:00
crefine abstract Haskell init parameters into constants 2014-11-06 18:48:36 +11:00
drefine drefine: Isabelle 2014 changes. 2014-09-24 12:21:10 +10:00
infoflow infoflow: remove s0_ptrs_distinct from Example_Valid_StateH 2014-11-19 16:01:49 +11:00
invariant-abstract Merge 'master' into 'isabelle-2014'. 2014-09-17 14:21:13 +10:00
refine abstract Haskell init parameters into constants 2014-11-06 18:48:36 +11:00
sep-capDL Merge branch 'master' into 'isabelle-2014'. 2014-09-23 14:31:33 +10:00
Makefile sync Makefile and test.xml 2014-11-23 19:54:59 +11:00
README.md integrate separation kernel config proofs 2014-08-13 22:08:46 +10:00
ROOT infoflow: fixed and added Example_Valid_StateH to testing 2014-11-18 17:39:17 +11:00
tests.xml sync Makefile and test.xml 2014-11-23 19:54:59 +11:00

README.md

Formal Proofs about seL4

This directory contains the formal proofs about seL4, which mostly prove properties about the various seL4 specifications.

Each such proof lives in its own subdirectory: