adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Gerwin Klein 76a69cda63 riscv refine: close sorry in KHeap_R 2019-11-12 18:28:39 +11:00
..
access-control proof: update for crunch changes 2019-10-14 17:23:41 +11:00
asmrefine asmrefine: improve initial debugging experience. 2019-11-12 14:25:58 +11:00
bisim global: isabelle update_cartouches 2019-06-14 11:41:21 +10:00
capDL-api proof: update for wp changes 2019-10-14 17:12:18 +11:00
crefine lib, x64 crefine: remove word lemma unat_ucast_8_64 2019-10-30 19:09:39 +11:00
drefine proof: update for crunch changes 2019-10-14 17:23:41 +11:00
infoflow proof: update for crunch changes 2019-10-14 17:23:41 +11:00
invariant-abstract riscv aspec: avoid type variable warning and freeindex increase 2019-11-12 18:28:38 +11:00
refine riscv refine: close sorry in KHeap_R 2019-11-12 18:28:39 +11:00
sep-capDL access-control, capDL-api, drefine, infoflow, sep-capDL, capDL: update for Isabelle2019 2019-06-13 16:22:33 +10:00
Makefile refine: move Orphanage to separate session, RefineOrphanage 2018-10-03 19:47:04 +10:00
README.md integrate separation kernel config proofs 2014-08-13 22:08:46 +10:00
ROOT global: isabelle update_cartouches 2019-06-14 11:41:21 +10:00
tests.xml regression: give SimplExportAndRefine more time 2019-06-25 12:29:41 +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: