Also, Robbert Krebbers's PhD thesis titled "The C standard formalized in Coq" [0]. From the summary: Our formal specification of C is faithful to the C11 stan

Also, Robbert Krebbers's PhD thesis titled "The C standard formalized in Coq" [0]. From the summary: Our formal specification of C is faithful to the C11 standard, which means it describes all undefined behaviors of C11. As a consequence, when one proves something about a given program with respect to our semantics, it should behave that way with any ostensibly C11 compliant compiler such as GCC or Clang. [0] http://robbertkrebbers.nl/thesis.html http://robbertkrebbers.nl/thesis.html