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