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.
COPYRIGHTfile in the distribution.
Installation instructions can be found in the
contained in the distribution.