adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Ryan Barry 8124b326b4 infoflow+crefine: refine arch split 
Signed-off-by: Ryan Barry <ryan.barry@unsw.edu.au>
 		2021-10-05 08:46:11 +11:00
..
access-control infoflow+access: Syscall arch split 2021-10-05 08:46:11 +11:00
asmrefine isabelle-2021 arm: update SimplExportAndRefine 2021-09-30 16:53:17 +10:00
bisim isabelle-2021: update Bisim 2021-09-30 16:53:17 +10:00
capDL-api isabelle-2021: update DSpecProofs 2021-09-30 16:53:17 +10:00
crefine infoflow+crefine: refine arch split 2021-10-05 08:46:11 +11:00
dpolicy isabelle-2021: update DPolicy 2021-09-30 16:53:17 +10:00
drefine isabelle-2021: update DRefine 2021-09-30 16:53:17 +10:00
infoflow infoflow+crefine: refine arch split 2021-10-05 08:46:11 +11:00
invariant-abstract ainvs: requalify for infoflow 2021-10-05 08:46:11 +11:00
refine isabelle-2021 riscv: update Refine 2021-09-30 16:53:17 +10:00
sep-capDL word_lib: remove unused theories 2021-09-30 16:53:17 +10:00
Makefile asmrefine: SimplExportOnly renamed 2020-11-09 21:07:44 +11:00
README.md license: provide documentation under CC-BY-SA-4.0 2020-03-16 14:19:15 +08:00
ROOT proof/ROOT infoflow arch split 2021-10-05 08:46:11 +11:00
tests.xml regression: increase CRefine timeout 2020-11-26 00:31:04 +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: