adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Miki Tanaka caf09bd3db aspec+ainvs: remove interrupt/irq from p_monad 
- preemption in C is not associated to an irq
- updating aspec to reflect this so that we can have irq-independent
  preemptions (needed in MCS)

- proof fix for the above: remove intr

Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>
 		2020-10-25 13:15:00 +11:00
..
access-control cleanup: remove stray diagnostic commands and comments 2020-06-08 20:41:10 +08:00
asmrefine asmrefine: add `heap_update` identity rule 2020-09-07 14:10:04 +10:00
bisim bisim: proof updates for new arch split function 2020-06-08 20:41:10 +08:00
capDL-api cleanup: remove stray diagnostic commands and comments 2020-06-08 20:41:10 +08:00
crefine riscv: rename sbadaddr -> stval 2020-08-26 15:24:06 +10:00
drefine drefine: make new arch function available 2020-06-08 20:41:10 +08:00
infoflow trivial: fix broken links 2020-08-10 15:48:34 +08:00
invariant-abstract aspec+ainvs: remove interrupt/irq from p_monad 2020-10-25 13:15:00 +11:00
refine riscv: rename sbadaddr -> stval 2020-08-26 15:24:06 +10:00
sep-capDL license: provide documentation under CC-BY-SA-4.0 2020-03-16 14:19:15 +08:00
Makefile regression: explain why `CKernel` depends on `design-spec` 2020-08-10 13:45:35 +10:00
README.md license: provide documentation under CC-BY-SA-4.0 2020-03-16 14:19:15 +08:00
ROOT crefine: arch split for Move theory files and move in lemmas 2020-03-20 13:42:43 +11:00
tests.xml tests: give more time to AInvs session 2020-09-10 16:09:38 +08: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: