History

Thomas Sewell cc4b4102b7 Add a facility for ignoring complex asm. To restore some previous functionality, add a mechanism by which an __asm__ statement too complex to be translated can still be ignored (handled as an empty statement). A demo file does this for a wrapper around "nop". Also use this facility to support legacy camkes-glue proofs which assume that the software interrupt operator "swi" doesn't break anything.		2016-12-01 17:08:00 +11:00
..
asmrefine	Handling of AsmStmt in c-parser, more tests.	2016-12-01 17:07:54 +11:00
autocorres	SELFOUR-421: fix coding style	2016-09-22 19:23:28 +10:00
c-parser	Add a facility for ignoring complex asm.	2016-12-01 17:08:00 +11:00
haskell-translator	SELFOUR-444: Adjust Haskell, new ghost data.	2016-11-02 11:19:09 +11: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	Make CParseTools depend on CParser	2016-07-20 18:02:13 +10: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.