Verifying Optimizations for Concurrent Programs

DOI10.4230/OASIcs.WPTE.2014.15zbMath1428.68124OpenAlexW2132396668MaRDI QIDQ5240132

William Mansky, Elsa L. Gunter

Publication date: 24 October 2019

Full work available at URL: http://drops.dagstuhl.de/opus/volltexte/2014/4586/pdf/p015-03-mansky.pdf

zbMATH Keywords

program transformationstemporal logicinteractive theorem provingrelaxed memory modelsoptimizing compilers

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• A formally verified compiler back-end
• A rely-guarantee-based simulation for verifying concurrent program transformations
• Relaxed-memory concurrency and verified compilation
• A Framework for Formal Verification of Compiler Optimizations

This page was built for publication: Verifying Optimizations for Concurrent Programs