CompCertO: compiling certified open C components
| Autor: | Jérémie Koenig, Zhong Shao |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Correctness
Game semantics Programming language Computer science Calling convention Interoperability 020207 software engineering 0102 computer and information sciences 02 engineering and technology computer.software_genre 01 natural sciences 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering Compiler Communications protocol computer Software verification Abstraction (linguistics) |
| Zdroj: | PLDI |
| DOI: | 10.1145/3453483.3454097 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|