adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Rafal Kolanski 4262cc231a asmrefine: teach div and sdiv handling to graph refine tactic 2016-11-15 12:11:01 +11:00
..
access-control ADT: add kernel entry/exit constraints on domain time left 2016-11-11 06:01:30 +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-242: update goal number based indentation in Fastpath_C 2016-11-15 12:11:01 +11:00
drefine ADT: add kernel entry/exit constraints on domain time left 2016-11-11 06:01:30 +11:00
infoflow ADT: add kernel entry/exit constraints on domain time left 2016-11-11 06:01:30 +11:00
invariant-abstract SELFOUR-242: invert bitfield scheduler and optimise fast path 2016-11-15 09:20:31 +11:00
refine SELFOUR-242: invert bitfield scheduler and optimise fast path 2016-11-15 09:20:31 +11:00
sep-capDL SELFOUR-276: Finish proofs for maximum controlled priority (MCP) 2016-10-05 02:43:41 +11:00
Makefile avoid `make` warning, remove SimplExportOnly from HEAPS 2015-11-20 16:02:14 +11:00
README.md integrate separation kernel config proofs 2014-08-13 22:08:46 +10:00
ROOT SELFOUR-444: Haskell implementation, begin refine. 2016-11-02 11:19:08 +11:00
tests.xml regression: bump timeouts further. All timeouts now multiples of 1hr. 2016-02-22 17:38:35 +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: