CompCertO: compiling certified open C components
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.
Topics & Concepts
Computer scienceCorrectnessInteroperabilityProgramming languageCertificationSemantics (computer science)Software engineeringRangingOperating systemLawPolitical scienceTelecommunicationsSecurity and Verification in ComputingLogic, programming, and type systemsDistributed systems and fault tolerance