History

Rafal Kolanski 3349303b14 cparser: add support for ARM_HYP platform: umm_heap specs These are copied verbatim from ARM as the word and pointer sizes are identical. These could be auto-generated by a Makefile, but a Makefile is not invoked when building CKernel.		2017-06-19 14:32:30 +10:00
..
asmrefine	Merge pull request #159 in SEL4/l4v from ~TSEWELL/l4v:length-1-array to master	2017-02-17 15:08:46 +11:00
autocorres	autocorres: prepare packaging scripts for release 1.3	2017-04-03 14:46:53 +10:00
c-parser	cparser: add support for ARM_HYP platform: umm_heap specs	2017-06-19 14:32:30 +10:00
haskell-translator	haskell translator: update caseconvs	2017-06-19 14:32:22 +10:00
proofcount	more Isabelle2015 update; AInvs up to (excluding) Syscall_AI	2015-04-18 21:51:26 +01:00
README.md	Added new proofcount tool to "tools" and removed old one from "lib".	2015-02-11 17:46:34 +11:00
ROOTS	Import release snapshot.	2014-07-14 21:32:44 +02:00
tests.xml	backport changes to ARM proofs from X64 work in progress	2017-01-27 08:31:07 +11:00

Proof Tools

This directory contains proof tools, most of which are used in one or more of the seL4 proofs. Each has its own directory:

asmrefine - Generic Isabelle/HOL part of the binary verification tool, for use in the seL4 Assembly Refinement Proof.
autocorres - Tool for easing manual proofs about C code, described in this PLDI '14 paper.
c-parser - Tool for translating C code into Isabelle/HOL, used to give seL4's C code its semantics in e.g. the seL4 C Refinement Proof.
haskell-translator - Tool for translating Haskell into Isabelle/HOL, used to generate the seL4 design specification.
proofcount - Tool for collecting metrics from finished proofs.