README.md
1Proof Tools
2===========
3
4This directory contains proof tools, most of which are used in one or
5more of the seL4 [proofs](../proof/). Each has its own directory:
6
7 * [asmrefine](asmrefine/) - Generic Isabelle/HOL part of the binary
8 verification tool, for use in the seL4
9 [Assembly Refinement Proof](../proof/asmrefine).
10
11 * [autocorres](autocorres/) - Tool for easing manual proofs about
12 C code, described in this [PLDI '14 paper][1].
13
14 * [c-parser](c-parser/) - Tool for translating C code into
15 Isabelle/HOL, used to give seL4's C code its semantics in e.g. the
16 seL4 [C Refinement Proof](../proof/crefine/).
17
18 * [haskell-translator](haskell-translator/) - Tool for translating
19 Haskell into Isabelle/HOL, used to generate the seL4
20 [design specification](../spec/design/).
21
22 * [proofcount](proofcount/) - Tool for collecting metrics from
23 finished proofs.
24
25 [1]: http://www.nicta.com.au/pub?id=7629 "Don't Sweat the Small Stuff: Formal Verification of C Code Without the Pain"
26
27