English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Verified compilation of open modules (i.e., modules whose functionalitydepends on other modules) provides a foundation for end-to-end verification ofmodular programs ubiquitous in contemporary software. However, despiteintensive investigation in this topic for decades, the proposed approaches arestill difficult to use in practice as they rely on assumptions about theinternal working of compilers which make it difficult for external users toapply the verification results. We propose an approach to verifiedcompositional compilation without such assumptions in the setting of verifyingcompilation of heterogeneous modules written in first-order languagessupporting global memory and pointers. Our approach is based on the memorymodel of CompCert and a new discovery that a Kripke relation with a notion ofmemory protection can serve as a uniform and composable semantic interface forthe compiler passes. By absorbing the rely-guarantee conditions on memoryevolution for all compiler passes into this Kripke Memory Relation and bypiggybacking requirements on compiler optimizations onto it, we getcompositional correctness theorems for realistic optimizing compilers asrefinements that directly relate native semantics of open modules and that areignorant of intermediate compilation processes. Such direct refinements supportall the compositionality and adequacy properties essential for verifiedcompilation of open modules. We have applied this approach to the fullcompilation chain of CompCert with its Clight source language and demonstratedthat our compiler correctness theorem is open to composition and intuitive touse with reduced verification complexity through end-to-end verification ofnon-trivial heterogeneous modules that may freely invoke each other (e.g.,mutually recursively).

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules (Technical Report)