A formalization of the C99 standard in HOL, isabelle and Coq

Abstract

We recently started the Formalin project to create a formal version of the C99 standard for the C programming language. We are writing three matching formalizations for the interactive theorem provers HOL4, Isabelle/HOL and Coq, that all closely follow the existing C99 standard text. The project runs from 2011 to 2015, and involves a full time PhD student, a half time researcher and several scientific advisors. The project differs from existing work in that our aim is to formalize the full C99 standard. This means that we treat the C preprocessor, the C standard library, floating point arithmetic, and 'dirty' C features like signal handling and volatile variables. Importantly, this means we also treat embedded C programs without explicit input/output. © 2011 Springer-Verlag.