Sciweavers

Share
CADE
2008
Springer

Bitfields and Tagged Unions in C: Verification through Automatic Generation

9 years 3 months ago
Bitfields and Tagged Unions in C: Verification through Automatic Generation
We present a tool for automatic generation of packed bitfields and tagged unions for systems-level C, along with automatic, machine checked refinement proofs in Isabelle/HOL. Our approach provides greater predictability than compiler-specific bitfield implementations, and provides a basis for formal reasoning about these typically non-type-safe operations. The tool is used in the implementation of the seL4 microkernel, and hence also in the lowest-level refinement step of the L4.verified project which aims to prove the functional correctness of seL4. Within seL4, it has eliminated the need for unions entirely.
David Cock
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors David Cock
Comments (0)
books