On the Use of Underspecified Data-Type Semantics for Type Safety in Low-Level Code

Hendrik Tews, Marcus Völp, Tjark Weber

In recent projects on operating-system verification, C and C++ data types are often formalized using a semantics that does not fully specify the precise byte encoding of objects. I…