@inproceedings{DBLP:conf/wrla/AlrahmanABL14,
  author    = {Yehia {Abd Alrahman} and
               Marina Andric and
               Alessandro Beggiato and
               Alberto Lluch{-}Lafuente},
  editor    = {Santiago Escobar},
  title     = {Can We Efficiently Check Concurrent Programs Under Relaxed Memory
               Models in Maude?},
  booktitle = {Rewriting Logic and Its Applications - 10th International Workshop,
               {WRLA} 2014, Held as a Satellite Event of ETAPS, Grenoble, France,
               April 5-6, 2014, Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {8663},
  pages     = {21-41},
  publisher = {Springer},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-319-12904-4\_2},
  doi       = {10.1007/978-3-319-12904-4\_2},
  abstract  = {Relaxed memory models offer suitable abstractions of the actual optimizations offered by multi-core architectures and by compilers of concurrent programming languages. Using such abstractions for verification purposes is challenging in part due to their inherent non-determinism which contributes to the state space explosion. Several techniques have been proposed to mitigate those problems so to make verification under relaxed memory models feasible. We discuss how to adopt some   of those techniques in a Maude-based approach to language prototyping, and suggest the use of other techniques that have been shown successful for similar verification purposes.}
}

{"_id":"XFG82B5E3mB55geoH","bibbaseid":"abdalrahman-andric-beggiato-lluchlafuente-canweefficientlycheckconcurrentprogramsunderrelaxedmemorymodelsinmaude-2014","author_short":["Abd Alrahman, Y.","Andric, M.","Beggiato, A.","Lluch-Lafuente, A."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Yehia"],"propositions":[],"lastnames":["Abd Alrahman"],"suffixes":[]},{"firstnames":["Marina"],"propositions":[],"lastnames":["Andric"],"suffixes":[]},{"firstnames":["Alessandro"],"propositions":[],"lastnames":["Beggiato"],"suffixes":[]},{"firstnames":["Alberto"],"propositions":[],"lastnames":["Lluch-Lafuente"],"suffixes":[]}],"editor":[{"firstnames":["Santiago"],"propositions":[],"lastnames":["Escobar"],"suffixes":[]}],"title":"Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude?","booktitle":"Rewriting Logic and Its Applications - 10th International Workshop, WRLA 2014, Held as a Satellite Event of ETAPS, Grenoble, France, April 5-6, 2014, Revised Selected Papers","series":"Lecture Notes in Computer Science","volume":"8663","pages":"21-41","publisher":"Springer","year":"2014","url":"https://doi.org/10.1007/978-3-319-12904-4\\_2","doi":"10.1007/978-3-319-12904-4_2","abstract":"Relaxed memory models offer suitable abstractions of the actual optimizations offered by multi-core architectures and by compilers of concurrent programming languages. Using such abstractions for verification purposes is challenging in part due to their inherent non-determinism which contributes to the state space explosion. Several techniques have been proposed to mitigate those problems so to make verification under relaxed memory models feasible. We discuss how to adopt some of those techniques in a Maude-based approach to language prototyping, and suggest the use of other techniques that have been shown successful for similar verification purposes.","bibtex":"@inproceedings{DBLP:conf/wrla/AlrahmanABL14,\n author = {Yehia {Abd Alrahman} and\n Marina Andric and\n Alessandro Beggiato and\n Alberto Lluch{-}Lafuente},\n editor = {Santiago Escobar},\n title = {Can We Efficiently Check Concurrent Programs Under Relaxed Memory\n Models in Maude?},\n booktitle = {Rewriting Logic and Its Applications - 10th International Workshop,\n {WRLA} 2014, Held as a Satellite Event of ETAPS, Grenoble, France,\n April 5-6, 2014, Revised Selected Papers},\n series = {Lecture Notes in Computer Science},\n volume = {8663},\n pages = {21-41},\n publisher = {Springer},\n year = {2014},\n url = {https://doi.org/10.1007/978-3-319-12904-4\\_2},\n doi = {10.1007/978-3-319-12904-4\\_2},\n abstract = {Relaxed memory models offer suitable abstractions of the actual optimizations offered by multi-core architectures and by compilers of concurrent programming languages. Using such abstractions for verification purposes is challenging in part due to their inherent non-determinism which contributes to the state space explosion. Several techniques have been proposed to mitigate those problems so to make verification under relaxed memory models feasible. We discuss how to adopt some of those techniques in a Maude-based approach to language prototyping, and suggest the use of other techniques that have been shown successful for similar verification purposes.}\n}\n","author_short":["Abd Alrahman, Y.","Andric, M.","Beggiato, A.","Lluch-Lafuente, A."],"editor_short":["Escobar, S."],"key":"DBLP:conf/wrla/AlrahmanABL14","id":"DBLP:conf/wrla/AlrahmanABL14","bibbaseid":"abdalrahman-andric-beggiato-lluchlafuente-canweefficientlycheckconcurrentprogramsunderrelaxedmemorymodelsinmaude-2014","role":"author","urls":{"Paper":"https://doi.org/10.1007/978-3-319-12904-4\\_2"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://lazkany.bitbucket.io/publication.bib","dataSources":["9BWFRLuir5vrfREwa"],"keywords":[],"search_terms":["efficiently","check","concurrent","programs","under","relaxed","memory","models","maude","abd alrahman","andric","beggiato","lluch-lafuente"],"title":"Can We Efficiently Check Concurrent Programs Under Relaxed Memory Models in Maude?","year":2014}