adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof
History
Gerwin Klein 5ae7cc23b1 aspec: msg_align_bits and related are arch independent 
While the numerical value is arch dependent, the definition and symbolic value
are not. This commit factors out the symbolic computation and only unfolds the
numeric value in the architecture dependent spec.
 		2018-08-06 11:22:51 +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 aspec: msg_align_bits and related are arch independent 2018-08-06 11:22:51 +10:00
drefine aspec: msg_align_bits and related are arch independent 2018-08-06 11:22:51 +10:00
infoflow aspec: msg_align_bits and related are arch independent 2018-08-06 11:22:51 +10:00
invariant-abstract aspec: message_info_to_data is mostly arch independent 2018-08-06 11:22:51 +10:00
refine aspec: message_info_to_data is mostly arch independent 2018-08-06 11:22:51 +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: