Verifying optimizations for concurrent programs

DOI10.4230/OASICS.WPTE.2014.15MaRDI QIDQ5240132zbMATH OpenOpenAlexFDO

Authors William Mansky, Elsa 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

temporal logicinteractive theorem provingprogram transformationsrelaxed memory modelsoptimizing compilers

Mathematics Subject Classification ID

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

Recommendations

• A Framework for Formal Verification of Compiler Optimizations
• CompCertTSO
• Compositional verification of compiler optimisations on relaxed memory
• Relaxed-memory concurrency and verified compilation
• Verified Compilation for Shared-Memory C

Cites work

• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3688686 (Why is no real title available?)
• A Framework for Formal Verification of Compiler Optimizations
• A formally verified compiler back-end
• A rely-guarantee-based simulation for verifying concurrent program transformations
• Relaxed-memory concurrency and verified compilation

Cited in

(10)

• Relaxed-memory concurrency and verified compilation
• Simulation Refinement for Concurrency Verification
• A rely-guarantee-based simulation for verifying concurrent program transformations
• Formalizing the LLVM intermediate representation for verified program transformations
• Efficient verification of sequential and concurrent C programs
• A verifying compiler for a multi-threaded object-oriented language
• Formalizing and checking thread refinement for data-race-free execution models
• Going beyond dual execution: MPC for functions with efficient verification
• Compositional verification of compiler optimisations on relaxed memory
• From Verification to Optimizations

This page was built for publication: Verifying optimizations for concurrent programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5240132)