@article{DBLP:journals/jacm/SevcikVNJS13,
  author       = {Jaroslav Sevc{\'{\i}}k and
                  Viktor Vafeiadis and
                  Francesco Zappa Nardelli and
                  Suresh Jagannathan and
                  Peter Sewell},
  title        = {CompCertTSO: {A} Verified Compiler for Relaxed-Memory Concurrency},
  journal      = {J. {ACM}},
  volume       = {60},
  number       = {3},
  pages        = {22:1--22:50},
  year         = {2013},
  url          = {https://doi.org/10.1145/2487241.2487248},
  doi          = {10.1145/2487241.2487248},
  timestamp    = {Mon, 28 Aug 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/jacm/SevcikVNJS13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

{"_id":"uEqrFkJhnw2TFMbbt","bibbaseid":"sevck-vafeiadis-nardelli-jagannathan-sewell-compcerttsoaverifiedcompilerforrelaxedmemoryconcurrency-2013","author_short":["Sevcík, J.","Vafeiadis, V.","Nardelli, F. Z.","Jagannathan, S.","Sewell, P."],"bibdata":{"bibtype":"article","type":"article","author":[{"firstnames":["Jaroslav"],"propositions":[],"lastnames":["Sevcík"],"suffixes":[]},{"firstnames":["Viktor"],"propositions":[],"lastnames":["Vafeiadis"],"suffixes":[]},{"firstnames":["Francesco","Zappa"],"propositions":[],"lastnames":["Nardelli"],"suffixes":[]},{"firstnames":["Suresh"],"propositions":[],"lastnames":["Jagannathan"],"suffixes":[]},{"firstnames":["Peter"],"propositions":[],"lastnames":["Sewell"],"suffixes":[]}],"title":"CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency","journal":"J. ACM","volume":"60","number":"3","pages":"22:1–22:50","year":"2013","url":"https://doi.org/10.1145/2487241.2487248","doi":"10.1145/2487241.2487248","timestamp":"Mon, 28 Aug 2023 01:00:00 +0200","biburl":"https://dblp.org/rec/journals/jacm/SevcikVNJS13.bib","bibsource":"dblp computer science bibliography, https://dblp.org","bibtex":"@article{DBLP:journals/jacm/SevcikVNJS13,\n author = {Jaroslav Sevc{\\'{\\i}}k and\n Viktor Vafeiadis and\n Francesco Zappa Nardelli and\n Suresh Jagannathan and\n Peter Sewell},\n title = {CompCertTSO: {A} Verified Compiler for Relaxed-Memory Concurrency},\n journal = {J. {ACM}},\n volume = {60},\n number = {3},\n pages = {22:1--22:50},\n year = {2013},\n url = {https://doi.org/10.1145/2487241.2487248},\n doi = {10.1145/2487241.2487248},\n timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},\n biburl = {https://dblp.org/rec/journals/jacm/SevcikVNJS13.bib},\n bibsource = {dblp computer science bibliography, https://dblp.org}\n}\n\n","author_short":["Sevcík, J.","Vafeiadis, V.","Nardelli, F. Z.","Jagannathan, S.","Sewell, P."],"key":"DBLP:journals/jacm/SevcikVNJS13","id":"DBLP:journals/jacm/SevcikVNJS13","bibbaseid":"sevck-vafeiadis-nardelli-jagannathan-sewell-compcerttsoaverifiedcompilerforrelaxedmemoryconcurrency-2013","role":"author","urls":{"Paper":"https://doi.org/10.1145/2487241.2487248"},"metadata":{"authorlinks":{}}},"bibtype":"article","biburl":"https://dblp.org/pid/j/SJagannathan.bib","dataSources":["w34nNagszyiH26GmA"],"keywords":[],"search_terms":["compcerttso","verified","compiler","relaxed","memory","concurrency","sevcík","vafeiadis","nardelli","jagannathan","sewell"],"title":"CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency","year":2013}