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
[thumbnail of main.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Batty
Date Deposited: 05 Apr 2018 14:36 UTC
Last Modified: 16 Feb 2021 13:54 UTC
Resource URI: (The current URI for this page, for reference purposes)
Batty, Mark:
  • Depositors only (login required):


Downloads per month over past year