adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Corey Lewis 284ef78ae9 lib: support crunching lifted monadic functions 
This also changes crunch to collect preconditions one at a time.

Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>
 		2021-07-12 15:09:50 +10:00
..
access-control access: move ExampleSystem 2021-06-21 20:10:32 +10:00
asmrefine riscv: fix CLZ and CTZ for riscv32 builds (#257) 2021-03-30 13:17:41 +11:00
bisim spec proof: resolve_address_bits'.simps[simp del] 2020-11-09 17:18:41 +11:00
capDL-api trivial: fix links to papers 2021-03-02 11:44:22 +11:00
crefine always use `addrFromKPPtr` for kernel addresses 2021-06-25 16:31:22 +10:00
dpolicy infoflow+dpolicy+cdl-refine: misc fixes 2021-06-21 20:10:32 +10:00
drefine always use `addrFromKPPtr` for kernel addresses 2021-06-25 16:31:22 +10:00
infoflow infoflow+dpolicy+cdl-refine: misc fixes 2021-06-21 20:10:32 +10:00
invariant-abstract lib: support crunching lifted monadic functions 2021-07-12 15:09:50 +10:00
refine refine: fix regression caused by bad theory import 2021-06-27 10:13:01 +10:00
sep-capDL trivial: fix links to papers 2021-03-02 11:44:22 +11: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 refine: fix regression caused by bad theory import 2021-06-27 10:13:01 +10: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: