adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Gerwin Klein 330e730fa3 retire old obsolete ADT refinement phrasing 
The observable state has been strengthened significantly years ago and
this theory has fallen into disrepair. The toplevel refinement statement
here was nicely concise for a paper, but the practical value is in the
much stronger corres statement, so instead of attempting proof
acrobatics with a new observable state, I'm retiring this theory.
 		2015-05-13 10:49:30 +02:00
..
access-control 2015 update for access 2015-05-06 13:46:20 -04:00
asmrefine Don't reuse the s_footprint_intvl theorem name. 2014-10-01 11:16:40 +10:00
bisim Isabelle2015 update: Bisim 2015-04-19 10:25:42 +01:00
capDL-api Merge branch 'master' into 'isabelle-2014'. 2014-09-23 14:31:33 +10:00
crefine adjust for seL4 rev 28d7fda6a9128efe 2015-01-10 08:34:52 +11:00
drefine retire old obsolete ADT refinement phrasing 2015-05-13 10:49:30 +02:00
infoflow re-establish InfoFlow; generalising ptable_xn 2014-11-28 08:58:57 +11:00
invariant-abstract Isabelle2015 update: AInvs 2015-04-19 10:25:21 +01:00
refine 2015 update for Refine 2015-05-12 17:17:31 +02: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 cleanup: there already is a separate Bisim session 2015-04-19 10:24:42 +01: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: