Aliasing restrictions of C11 formalized in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre la semántica del lenguaje C titulado Aliasing restrictions of C11 formalized in Coq.

Su autor es Robbert Krebbers (de la Radboud University Nijmegen, Holanda).

Su resumen es

The C11 standard of the C programming language describes dynamic typing restrictions on memory operations to make more effective optimizations based on alias analysis possible. These restrictions are subtle due to the low-level nature of C, and have not been treated in a formal semantics before. We present an executable formal memory model for C that incorporates these restrictions, and at the same time describes required low-level operations.

Our memory model and essential properties of it have been fully formalized using the Coq proof assistant.

Este trabajo forma parte del proyecto CH₂O cuyo objetivo es la formalización del estándard C11 del lenguaje de programación C.

El trabajo se presentará en el CPP 2013 (3rd International Conference on Certified Programs and Proofs).

El código de las correspondientes teorías en Coq se encuentra aquí.