adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Gerwin Klein 8c19ee35b0 proof/ROOT: comment out unused AutoLevity sessions 2018-08-20 09:06:34 +10:00
..
access-control globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
asmrefine globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
bisim globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
capDL-api globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
crefine globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
drefine globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
infoflow globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
invariant-abstract globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
refine x64 refine: add IOPortControl to EmptyFail_H 2018-08-20 09:06:34 +10:00
sep-capDL globally use session-qualified imports; add Lib session 2018-08-20 09:06:34 +10:00
Makefile proof/Makefile: add SimplExport* dependencies 2018-07-24 11:38:40 +10:00
README.md integrate separation kernel config proofs 2014-08-13 22:08:46 +10:00
ROOT proof/ROOT: comment out unused AutoLevity sessions 2018-08-20 09:06:34 +10:00
tests.xml lib: make Lib session a test dependency 2018-08-20 09:06:34 +10: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: