Per-Location Simulation

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Simulation/bisimulation is one of the most widely used frameworks for proving program equivalence/semantic preservation. In this paper, we propose a new per-location simulation (PLS) relation that is simple and suitable for proving that a compiled program semantically preserves its original program under a CFG-based language with a real-world, C/C++ like, weak memory model. To the best of our knowledge, PLS is the first simulation framework weaker than the CompCert[26]/CompCertTSO[47] one that is used for proving compiler correctness. With a combination of PLS, the compiler proof-framework Morpheus[34], and a language semantics with a weak memory model, we are able to prove that programs are semantically preserved through a transformation. All the definitions and proofs have been implemented in Isabelle/HOL.

Original languageEnglish (US)
Title of host publicationNASA Formal Methods - 12th International Symposium, NFM 2020, Proceedings
EditorsRitchie Lee, Susmit Jha, Anastasia Mavridou
PublisherSpringer
Pages267-287
Number of pages21
ISBN (Print)9783030557539
DOIs
StatePublished - 2020
Event12th International Symposium on NASA Formal Methods, NFM 2020 - Moffett Field, United States
Duration: May 11 2020May 15 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12229 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference12th International Symposium on NASA Formal Methods, NFM 2020
Country/TerritoryUnited States
CityMoffett Field
Period5/11/205/15/20

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Per-Location Simulation'. Together they form a unique fingerprint.

Cite this