adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Japheth Lim 18e0d934cc refine: move Orphanage to separate session, RefineOrphanage 
Previously, the build system conditionally included Orphanage, but only
when built from run_tests. This meant that a plain ‘isabelle jedit’ or
‘make Refine’ would see a different session definition, resulting in a
slow rebuild.

NB: editing Orphanage now requires -l Refine instead of -l BaseRefine.
 		2018-10-03 19:47:04 +10:00
..
access-control Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM. 2018-09-19 16:18:09 +10:00
asmrefine Isabelle2018: new AsmRefine session + test 2018-08-20 09:06:36 +10:00
bisim Isabelle2018: new "op x" syntax; now is "(x)" 2018-08-20 09:06:35 +10:00
capDL-api lib+sysinit: add extended separation algebra and forward reasoning tactics 2018-09-18 12:01:52 +10:00
crefine Minor adjustments to the patch for selfour-1491. 2018-09-21 10:09:49 +10:00
drefine Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM. 2018-09-19 16:18:09 +10:00
infoflow Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM. 2018-09-19 16:18:09 +10:00
invariant-abstract Updated specs and proofs for SELFOUR-1491: control IRQ triggering on ARM. 2018-09-19 16:18:09 +10:00
refine refine: move Orphanage to separate session, RefineOrphanage 2018-10-03 19:47:04 +10:00
sep-capDL lib+sysinit: add extended separation algebra and forward reasoning tactics 2018-09-18 12:01:52 +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 refine: move Orphanage to separate session, RefineOrphanage 2018-10-03 19:47:04 +10:00
tests.xml refine: move Orphanage to separate session, RefineOrphanage 2018-10-03 19:47:04 +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: