adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
MiladKetabi d934d25269 proof update for SELFOUR-1187: seL4 setPriority should attempt a direct schedule 
Prior to this commit the kernel would always trigger a full reschedule
on setPriority. This change allows the kernel to attempt a direct
switch, avoiding invoking the scheduler.
 		2019-10-06 18:31:19 +11:00
..
access-control proof update for SELFOUR-1187: seL4 setPriority should attempt a direct schedule 2019-10-06 18:31:19 +11:00
asmrefine global: isabelle update_cartouches 2019-06-14 11:41:21 +10:00
bisim global: isabelle update_cartouches 2019-06-14 11:41:21 +10:00
capDL-api global: isabelle update_cartouches 2019-06-14 11:41:21 +10:00
crefine proof update for SELFOUR-1187: seL4 setPriority should attempt a direct schedule 2019-10-06 18:31:19 +11:00
drefine proof update for SELFOUR-1187: seL4 setPriority should attempt a direct schedule 2019-10-06 18:31:19 +11:00
infoflow proof update for SELFOUR-1187: seL4 setPriority should attempt a direct schedule 2019-10-06 18:31:19 +11:00
invariant-abstract proof update for SELFOUR-1187: seL4 setPriority should attempt a direct schedule 2019-10-06 18:31:19 +11:00
refine proof update for SELFOUR-1187: seL4 setPriority should attempt a direct schedule 2019-10-06 18:31:19 +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: