text: abstract-state machines by gurevich and huggins [5], norrish’s c ++ semantics in hol4 [12] and the operating-system verification projects vfiasco [7], l4.verified [10] and
  robin [16] all use a semantics of c or c ++ data types that employs (untyped) byte sequences to encode
  typed values for storing them in memory. an underspecified, partial function converts byte sequences
  back into typed values.
  we use the term underspecified data-type semantics to refer to such a semantics of data types that converts between typed values and untyped byte sequences while leaving the precise conversion functions
  underspecified. with an underspecified data-type semantics, it is unknown during program verification
  which specific bytes are written to memory.
  the main ingredients of underspecified data-type semantics are two functions — to byte and
  from byte — that convert between typed values and byte sequences. the function from byte is in general
  partial, because not every byte sequence encodes a typed value. for instance, consider a representation
  of integers that uses a parity bit: from byteint would be undefined for byte sequences with invalid parity.
  underspecified data-type semantics are relevant for the verification of low-level systems code. this
  includes code that needs to maintain hardware-controlled data structures, e.g., page directories, or that
  contains its own memory allocator. type and memory safety of such low-level code depend on its
  functional correctness and are undecidable in general. for this reason, type safety for such code can only
  be established by logical reasoning and not by a conventional type system. as a consequence, this paper
  focuses on data-type semantics instead of improving the type system for, e.g., c ++.
  having to establish type correctness by verification is not as bad as it first sounds. with suitable
  lemmas, type correctness can be proved automatically for those parts of the code that are statically type
  ∗ this work was in part funded by the european commission through pasr grant 104600, by the deutsche forschungsgemeinschaft through the quaos project, and by the swedish research council.