Trace-Relating Compiler Correctness and Secure Compilation
From MaRDI portal
Publication:5041085
DOI10.1007/978-3-030-44914-8_1OpenAlexW3022052771MaRDI QIDQ5041085
Marco Patrignani, Deepak Garg, Carmine Abate, Roberto Blanco, Jérémy Thibault, Adrien Durier, Cătălin Hriţcu, Ştefan Ciobâcă, Éric Tanter
Publication date: 13 October 2022
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1907.05320
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- CompCertTSO
- Determinacy \(\to\) (observation equivalence \(=\) trace equivalence)
- An algebraic construction of predicate transformers
- Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
- VST-Floyd: a separation logic tool to verify correctness of C programs
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data
- Fully abstract trace semantics for protected module architectures
- Safety of abstract interpretations for free, via logical relations and Galois connections
- Whither specifications as programs
- Verified compilation of floating-point computations
- A formally verified compiler back-end
- A reflection on call-by-value
- Compositional CompCert
- Lightweight verification of separate compilation
- Formalizing the LLVM intermediate representation for verified program transformations
- Pilsner: a compositionally verified compiler for a higher-order imperative language
- A categorical model for higher order imperative programming
- The verified CakeML compiler backend
- Hyperhierarchy of Semantics - A Formal Framework for Hyperproperties Verification
- Programming Languages and Systems
- CompCertTSO
- A kripke logical relation between ML and assembly
- Verified Compilation for Shared-Memory C
This page was built for publication: Trace-Relating Compiler Correctness and Secure Compilation
