Skip to main content

Compositional Verification of Compiler Optimisations on Relaxed Memory

Dodds, Mike, Batty, Mark, Gotsman, Alexey (2018) Compositional Verification of Compiler Optimisations on Relaxed Memory. In: Lecture Notes in Computer Science. Programming Languages and Systems: 27th European Symposium on Programming, ESOP 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 Proceedings. 10801. Springer ISBN 978-3-319-89883-4. (doi:10.1007/978-3-319-89884-1_36) (KAR id:66630)

PDF Author's Accepted Manuscript
Language: English
Download (618kB) Preview
Official URL


This paper is about verifying program transformations on an axiomatic

present particular challenges for verifying program transformations, because

For a block of code being transformed, we define a denotation from its behaviour

code block with the rest of the program both through local and global variables,

prove that a transformation does not introduce new program behaviours by comparing

by examining only representative contexts, transformations are verified

verified. We cover several tricky aspects of C/C++-style memory models, including

We also define a variant of our denotation that is finite at the cost of losing full

tool and app

Item Type: Conference or workshop item (Proceeding)
DOI/Identification number: 10.1007/978-3-319-89884-1_36
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Mark Batty
Date Deposited: 05 Apr 2018 14:36 UTC
Last Modified: 20 Feb 2020 04:09 UTC
Resource URI: (The current URI for this page, for reference purposes)
Batty, Mark:
  • Depositors only (login required):


Downloads per month over past year