Publications
Detailed Information
CompCertM: CompCert with C-assembly linking and lightweight modular verification
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Song, Youngju | - |
dc.contributor.author | Cho, Minki | - |
dc.contributor.author | Kim, Dongjoo | - |
dc.contributor.author | Kim, Yonghyun | - |
dc.contributor.author | Kang, Jeehoon | - |
dc.contributor.author | Hur, Chung-Kil | - |
dc.date.accessioned | 2023-10-30T02:04:01Z | - |
dc.date.available | 2023-10-30T02:04:01Z | - |
dc.date.created | 2020-09-21 | - |
dc.date.issued | 2020-01 | - |
dc.identifier.citation | Proceedings of the ACM on Programming Languages, Vol.4 No.POPL, p. 23 | - |
dc.identifier.issn | 2475-1421 | - |
dc.identifier.uri | https://hdl.handle.net/10371/196036 | - |
dc.description.abstract | Supporting multi-language linking such as linking C and handwritten assembly modules in the verified compiler CompCert requires a more compositional verification technique than that used in CompCert just supporting separate compilation. The two extensions, CompCertX and Compositional CompCert, supporting multi-language linking take different approaches. The former simplifies the problem by imposing restrictions that the source modules should have no mutual dependence and be verified against certain well-behaved specifications. On the other hand, the latter develops a new verification technique that directly solves the problem but at the expense of significantly increasing the verification cost. In this paper, we develop a novel lightweight verification technique, called RUSC (Refinement Under Self-related Contexts), and demonstrate how RUSC can solve the problem without any restrictions but still with low verification overhead. For this, we develop CompCertM, a full extension of the latest version of CompCert supporting multi-language linking. Moreover, we demonstrate the power of RUSC as a program verification technique by modularly verifying interesting programs consisting of C and handwritten assembly against their mathematical specifications. | - |
dc.language | 영어 | - |
dc.publisher | Association for Computing Machinery | - |
dc.title | CompCertM: CompCert with C-assembly linking and lightweight modular verification | - |
dc.type | Article | - |
dc.identifier.doi | 10.1145/3371091 | - |
dc.citation.journaltitle | Proceedings of the ACM on Programming Languages | - |
dc.identifier.wosid | 000685202400024 | - |
dc.identifier.scopusid | 2-s2.0-85089765541 | - |
dc.citation.number | POPL | - |
dc.citation.startpage | 23 | - |
dc.citation.volume | 4 | - |
dc.description.isOpenAccess | Y | - |
dc.contributor.affiliatedAuthor | Hur, Chung-Kil | - |
dc.type.docType | Article | - |
dc.description.journalClass | 1 | - |
dc.subject.keywordAuthor | Compositional Compiler Verification | - |
dc.subject.keywordAuthor | CompCert | - |
dc.subject.keywordAuthor | Multi-Language Linking | - |
- Appears in Collections:
- Files in This Item:
- There are no files associated with this item.
Item View & Download Count
Items in S-Space are protected by copyright, with all rights reserved, unless otherwise indicated.