adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Matthew Brecknell 2f4b822da9 x64: configure arch-specific array types 2017-06-22 17:24:53 +10:00
..
access-control lib: new invariant syntax "f {|P|}" 2017-03-17 11:13:41 +11:00
asmrefine x64: configure arch-specific array types 2017-06-22 17:24:53 +10:00
bisim wp: update the proofs for the new wp/wpc/wpsimp 2017-03-16 19:39:11 +11:00
capDL-api wp: update the proofs for the new wp/wpc/wpsimp 2017-03-16 19:39:11 +11:00
crefine x64: configure arch-specific array types 2017-06-22 17:24:53 +10:00
drefine wp: update the proofs for the new wp/wpc/wpsimp 2017-03-16 19:39:11 +11:00
infoflow wp: update the proofs for the new wp/wpc/wpsimp 2017-03-16 19:39:11 +11:00
invariant-abstract x64: ainvs: fix broken proofs from strengthening of wellformed_pde et al 2017-04-21 17:17:21 +10:00
refine x64 refine: fix proofs after rebase and spec updates 2017-04-24 23:58:05 +10:00
sep-capDL wp_cleanup: update proofs for new wp behaviour 2017-01-13 14:04:15 +01:00
Makefile x64: configure default proof/Makefile targets 2017-04-29 15:31:29 +10:00
README.md integrate separation kernel config proofs 2014-08-13 22:08:46 +10:00
ROOT x64 refine: add a RefineOnly image which skips Orphanage 2017-04-24 23:58:05 +10:00
tests.xml x64: create arch-specific CKernel 2017-06-22 17:24:53 +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: