Compositional CompCert

Abstract

This paper reports on the development of Compositional CompCert, the first verified separate compiler for C.

Document Details

• Document Type: Pub Defense Publication
• Publication Date: Jan 14, 2015
• Source ID: 10.1145/2775051.2676985

Entities

People

• Andrew Appel
• Gordon Stewart
• Lennart Beringer
• Santiago Cuellar

Organizations

• Defense Advanced Research Projects Agency
• Princeton University