23/06/2021

CompCertO: Compiling Certified Open C Components

Jérémie Koenig, Zhong Shao

Keywords: Compositional Compiler Correctness, Game Semantics, Simulation Convention, Language Interface

Abstract Paper Code Similar Papers

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.

The video of this talk cannot be embedded. You can watch it here:
https://slideslive.com/38956322
(Link will open in new window)
 0
 0
 0
 0
  Share    
This is an embedded video. Talk and the respective paper are published at PLDI 2021 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd Characters remaining: 140

Similar Papers

 0
 0
 0
 0
 24:00 
 0
 0
 0
 0
 16:16 
 0
 0
 0
 0
 14:59 
 0
 0
 0
 0
 16:16 
 0
 0
 0
 0
 14:58 
 0
 0
 0
 0
 19:42 
 0
 0
 0
 0
 10:06 
 0
 0
 0
 0
 18:50 
 0
 0
 0
 0
 21:05 
 0
 0
 0
 0
 4:34 
 0
 0
 0
 0
 14:56 
 0
 0
 0
 0
 15:43 
 0
 0
 0
 0
 16:14 
 0
 0
 0
 0
 4:27 
 0
 0
 0
 0
 15:16 
 0
 0
 0
 0
 23:25 
 0
 0
 0
 0
 15:28 
 0
 0
 0
 0
 15:50 
 0
 0
 0
 0
 14:49 
 0
 0
 0
 0
 15:00 
 0
 0
 0
 0
 5:10 
 0
 0
 0
 0
 6:27 
 0
 0
 0
 0
 16:29 
 0
 0
 0
 0
 6:16 
 0
 0
 0
 0
 19:42 
 0
 0
 0
 0
 12:17 
 0
 0
 0
 0
 16:04 
 0
 0
 0
 0
 19:10 
 0
 0
 0
 0
 12:40 
 0
 0
 0
 0
 22:53 
 0
 0
 0
 0
 14:10 
 0
 0
 0
 0
 21:37 
 0
 0
 0
 0
 4:34 
 0
 0
 0
 0
 15:00 
 0
 0
 0
 0
 12:34 
 0
 0
 0
 0
 21:13 
 0
 0
 0
 0
 8:44 
 0
 0
 0
 0
 21:09 
 0
 0
 0
 0
 16:07 
 0
 0
 0
 0
 13:28