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 the COPYRIGHT file in the distribution.

Download

• bitfield_gen-2013-12-4.tar.gz

Installation instructions can be found in the README file contained in the distribution.