adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Gerwin Klein 24c0c5c390 spec+proof: use generated config constants 
This includes replacing previous ASpec names for such constants with
the names used in Haskell/ExecSpec to avoid duplication. This also
makes some of the proofs slightly more generic.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
 		2021-12-23 14:54:13 +11:00
..
access-control spec+proof: use generated config constants 2021-12-23 14:54:13 +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 spec+proof: use generated config constants 2021-12-23 14:54:13 +11:00
dpolicy various: resolve some new fixmes 2021-11-12 09:39:16 +11:00
drefine spec+proof: use generated config constants 2021-12-23 14:54:13 +11:00
infoflow spec+proof: use generated config constants 2021-12-23 14:54:13 +11:00
invariant-abstract spec+proof: use generated config constants 2021-12-23 14:54:13 +11:00
refine spec+proof: use generated config constants 2021-12-23 14:54:13 +11: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: