adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Japheth Lim 8392624f6c infoflow: hacky speedups for Noninterference.thy 
This speeds up a bunch of the slowest uwr and automaton proofs in
Noninterference, mainly by adjusting the simp depth limit to avoid
unneeded backtracking. Inspired by a rant from Tom Sewell.
 		2018-08-02 16:53:04 +10:00
..
access-control access, infoflow: cleanup from previous commit; some style cleanup 2018-08-02 16:53:04 +10:00
asmrefine asmrefine: ctcb_offset AUXUPD 2018-03-26 14:37:22 +11:00
bisim Proof update for crunch changes 2018-04-04 14:13:55 +10:00
capDL-api Proof update for crunch changes 2018-04-04 14:13:55 +10:00
crefine arm-hyp: update proofs for TPIDRUR[OW]/TLS_BASE preservation 2018-07-12 23:38:58 +10:00
drefine x64: more abstract specs and invariants for ASIDs 2018-07-05 16:23:15 +10:00
infoflow infoflow: hacky speedups for Noninterference.thy 2018-08-02 16:53:04 +10:00
invariant-abstract x64: ainvs+refine: fix up proofs for decodeX64FrameInvocation changes 2018-07-05 16:23:15 +10:00
refine x64: refine: fix fallout from decodeX64PageInvocation change 2018-07-05 16:23:15 +10:00
sep-capDL Many proof repairs. 2018-03-16 14:57:51 +11:00
Makefile proof/Makefile: add SimplExport* dependencies 2018-07-24 11:38:40 +10:00
README.md integrate separation kernel config proofs 2014-08-13 22:08:46 +10:00
ROOT infoflow: add InfoFlow_Image_Toplevel 2017-11-27 21:00:14 +11:00
tests.xml proofs: record tests.xml dependencies for SepTacticsExamples 2018-06-27 10:06:48 +02: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: