Code and Proof Co-Generation Tool for Bitfields
What is this?
Here you can download a DSL compiler, used to define and manipulate bitfields (in C), in a structured way, with automatic generation of Isabelle/HOL correctness proofs.
This software was developed as part of the L4.verified project, where it was used to generate code to create and access tagged unions of packed bitfields, in a manner consistent with the C translation used in the project, together with automatically generated (and proved) correctness theorems. For further details, see the associated publication: Cock_08.
Limitations
This software is a research prototype, and thus is likely to contain bugs, and unimplemented features. Notwithstanding this, the proofs of correctness generated are guaranteed correct: this is translation validation. To build the included examples, you will need the a version of the C parser dated at least 31/12/2013, and a compatible version of Isabelle/HOL.License
The license for the tools can be found in theCOPYRIGHT file in the
distribution.
Download
Installation instructions can be found in the README file
contained in the distribution.