-
CompCertTSO: A Verified Compiler for Relaxed-Memory
Concurrency.
Jaroslav Ševčík, Viktor Vafeiadis, Francesco
Zappa Nardelli, Suresh Jagannathan, and Peter Sewell.
J. ACM, 60(3):22:1--22:50, June 2013.
[ bib |
doi |
project page |
pdf |
abstract ]
-
CompCert-TSO release, Version 1.12, Jaroslav
Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh
Jagannathan, and Peter Sewell, August 2011.
[ bib |
project page |
.html ]
-
Relaxed-Memory Concurrency and Verified
Compilation.
Jaroslav Ševčík, Viktor Vafeiadis, Francesco
Zappa Nardelli, Suresh Jagannathan, and Peter Sewell.
In POPL 2011.
[ bib |
doi |
project page |
pdf |
abstract ]