The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

CompCertO: Compiling Certified Open C Components

Last modified: Thu Apr 22 00:31:09 2021 GMT.

Authors

Jérémie Koenig
Zhong Shao

Abstract

Since the introduction of CompCert, researchers have been refining its language semantics and correctness theorem, and used them as components in software verification efforts. Meanwhile, artifacts ranging from CPU designs to network protocols have been successfully verified, and there is interest in making them interoperable to tackle end-to-end verification at an even larger scale.

Recent work shows that a synthesis of game semantics, refinement-based methods, and abstraction layers has the potential to serve as a common theory of certified components. Integrating certified compilers to such a theory is a critical goal. However, none of the existing variants of CompCert meets the requirements we have identified for this task.

CompCertO extends the correctness theorem of CompCert to characterize compiled program components directly in terms of their interaction with each other. Through a careful and compositional treatment of calling conventions, this is achieved with minimal effort.

Published

In Proc. 2021 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'21), Virtual, Canada. 15 pages, June 2021.
  • Conference Paper [PDF]
  • Technical Report [PDF]

  • Copyright © 1996-2021 The FLINT Group <flint at cs dot yale dot edu>
    Yale University Department of Computer Science
    Validate this page
    colophon