adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Gerwin Klein 9f32001c78 arm-hyp: enable quick_and_dirty for snd CBaseRefine image 2017-06-19 14:32:35 +10:00
..
access-control arm: refactor sanitise_register to take a bool instead of a kernel_object 2017-05-03 21:51:57 +10:00
asmrefine Isabelle2016-1: configure c-parser with faster string comparisons 2017-01-05 14:27:44 +11: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 arm-hyp crefine: add ccorres_pre rules for vcpu/tcb 2017-06-19 14:32:35 +10:00
drefine arm: refactor sanitise_register to take a bool instead of a kernel_object 2017-05-03 21:51:57 +10:00
infoflow arm: refactor sanitise_register to take a bool instead of a kernel_object 2017-05-03 21:51:57 +10:00
invariant-abstract arm-hyp ainvs: update for do_flush 2017-06-19 14:32:32 +10:00
refine arm-hyp refine: various fixes and renames for obj_at' related rules 2017-06-19 14:32:34 +10:00
sep-capDL wp_cleanup: update proofs for new wp behaviour 2017-01-13 14:04:15 +01:00
Makefile refine: add intermediate BaseRefine2 session for small machines 2017-06-19 14:32:29 +10:00
README.md integrate separation kernel config proofs 2014-08-13 22:08:46 +10:00
ROOT arm-hyp: enable quick_and_dirty for snd CBaseRefine image 2017-06-19 14:32:35 +10:00
tests.xml design: Update Makefiles + tests.xml to auto-generate the design spec 2017-05-12 12:50:49 +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: