adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Miki Tanaka f8f88c6952 SELFOUR-553: Change Spec according to C code and fix ASpec and AInvs 2016-11-18 16:19:14 +11:00
..
access-control SELFOUR-64: Remove general Recycle operation 2016-11-18 14:11:12 +11:00
asmrefine asmrefine: teach div and sdiv handling to graph refine tactic 2016-11-15 12:11:01 +11:00
bisim add workaround for building documents with TeX Live 2016 [VER-622] 2016-07-22 07:48:08 +10:00
capDL-api SELFOUR-444: fix DSpecProofs and SysInit 2016-11-02 11:19:10 +11:00
crefine SELFOUR-64: Remove general Recycle operation 2016-11-18 14:11:12 +11:00
drefine SELFOUR-64: Remove general Recycle operation 2016-11-18 14:11:12 +11:00
infoflow SELFOUR-64: Remove general Recycle operation 2016-11-18 14:11:12 +11:00
invariant-abstract SELFOUR-553: Change Spec according to C code and fix ASpec and AInvs 2016-11-18 16:19:14 +11:00
refine SELFOUR-553: Change Spec according to C code and fix ASpec and AInvs 2016-11-18 16:19:14 +11:00
sep-capDL SELFOUR-276: Finish proofs for maximum controlled priority (MCP) 2016-10-05 02:43:41 +11:00
Makefile l4v: Add intermediate image for InfoFlowC. 2016-11-16 09:12:18 +11:00
README.md integrate separation kernel config proofs 2014-08-13 22:08:46 +10:00
ROOT l4v: Add intermediate image for InfoFlowC. 2016-11-16 09:12:18 +11:00
tests.xml Regression: removing unnecessary dependencies 2016-11-16 13:59:20 +11: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: