Skip to main content

Code and Proof Co-Generation Tool for Bitfields

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.


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.


The license for the tools can be found in the COPYRIGHT file in the distribution.


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

Served by Apache on Linux on seL4.