{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:12:16Z","timestamp":1767928336427,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314649","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"1117-1132","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["Verification of programs under the release-acquire semantics"],"prefix":"10.1145","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[{"name":"Uppsala University, Sweden"}]},{"given":"Jatin","family":"Arora","sequence":"additional","affiliation":[{"name":"IIT Bombay, India"}]},{"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[{"name":"Uppsala University, Sweden"}]},{"given":"Shankaranarayanan","family":"Krishna","sequence":"additional","affiliation":[{"name":"IIT Bombay, India"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Ahmed Bouajjani, and Tuan Phong Ngo.","author":"Abdulla Parosh Aziz","year":"2017","unstructured":"Parosh Aziz Abdulla , Mohamed Faouzi Atig , Ahmed Bouajjani, and Tuan Phong Ngo. 2017 . Context-Bounded Analysis for POWER. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II (Lecture Notes in Computer Science), Axel Legay and Tiziana Margaria (Eds.), Vol. 10206 . Springer , 56\u201374. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. 2017. Context-Bounded Analysis for POWER. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II (Lecture Notes in Computer Science), Axel Legay and Tiziana Margaria (Eds.), Vol. 10206. Springer, 56\u201374."},{"key":"e_1_3_2_2_2_1","volume-title":"ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings (Lecture Notes in Computer Science), Dang Van Hung and Mizuhito Ogawa (Eds.)","volume":"8172","author":"Abdulla Parosh Aziz","year":"2013","unstructured":"Parosh Aziz Abdulla , Mohamed Faouzi Atig , and Jonathan Cederberg . 2013 . Analysis of Message Passing Programs Using SMT-Solvers. In Automated Technology for Verification and Analysis - 11th International Symposium , ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings (Lecture Notes in Computer Science), Dang Van Hung and Mizuhito Ogawa (Eds.) , Vol. 8172 . Springer, 272\u2013286. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jonathan Cederberg. 2013. Analysis of Message Passing Programs Using SMT-Solvers. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings (Lecture Notes in Computer Science), Dang Van Hung and Mizuhito Ogawa (Eds.), Vol. 8172. Springer, 272\u2013286."},{"key":"e_1_3_2_2_3_1","first-page":"1","article-title":"Optimal stateless model checking under the release-acquire semantics","volume":"135","author":"Abdulla Parosh Aziz","year":"2018","unstructured":"Parosh Aziz Abdulla , Mohamed Faouzi Atig , Bengt Jonsson , and Tuan Phong Ngo . 2018 . Optimal stateless model checking under the release-acquire semantics . PACMPL 2, OOPSLA , 135 : 1 \u2013 135 :29. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan Phong Ngo. 2018. Optimal stateless model checking under the release-acquire semantics. PACMPL 2, OOPSLA, 135:1\u2013135:29.","journal-title":"PACMPL 2, OOPSLA"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_2_5_1","unstructured":"ARM. 2012. ARM architecture reference manual ARMv7-A and ARMv7-R edition.  ARM. 2012. ARM architecture reference manual ARMv7-A and ARMv7-R edition."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706303"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_2"},{"key":"e_1_3_2_2_8_1","volume-title":"CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.)","volume":"6806","author":"Atig Mohamed Faouzi","year":"2011","unstructured":"Mohamed Faouzi Atig , Ahmed Bouajjani , and Gennaro Parlato . 2011 . Getting Rid of Store-Buffers in TSO Analysis. In Computer Aided Verification - 23rd International Conference , CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.) , Vol. 6806 . Springer, 99\u2013115. Mohamed Faouzi Atig, Ahmed Bouajjani, and Gennaro Parlato. 2011. Getting Rid of Store-Buffers in TSO Analysis. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.), Vol. 6806. Springer, 99\u2013115."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_28"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926432"},{"key":"e_1_3_2_2_13_1","unstructured":"IBM. May 2013. Power ISATM version 2.07.  IBM. May 2013. Power ISATM version 2.07."},{"key":"e_1_3_2_2_14_1","unstructured":"Intel. 2014. Intel 64 and IA-32 architectures software developer\u2019s manual.  Intel. 2014. Intel 64 and IA-32 architectures software developer\u2019s manual."},{"key":"e_1_3_2_2_15_1","volume-title":"Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs. In 30th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2015","author":"Inverso Omar","year":"2015","unstructured":"Omar Inverso , Truc L. Nguyen , Bernd Fischer , Salvatore La Torre , and Gennaro Parlato . 2015 . Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs. In 30th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2015 , Lincoln, NE, USA , November 9-13, 2015, Myra B. Cohen, Lars Grunske, and Michael Whalen (Eds.). IEEE Computer Society, 807\u2013812. Omar Inverso, Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2015. Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs. In 30th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, November 9-13, 2015, Myra B. Cohen, Lars Grunske, and Michael Whalen (Eds.). IEEE Computer Society, 807\u2013812."},{"key":"e_1_3_2_2_16_1","volume-title":"Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In 31st European Conference on Object-Oriented Programming, ECOOP 2017","volume":"74","author":"Kaiser Jan-Oliver","year":"2017","unstructured":"Jan-Oliver Kaiser , Hoang-Hai Dang , Derek Dreyer , Ori Lahav , and Viktor Vafeiadis . 2017 . Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In 31st European Conference on Object-Oriented Programming, ECOOP 2017 , June 19-23, 2017, Barcelona, Spain (LIPIcs), Peter M\u00fcller (Ed.) , Vol. 74 . Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 17:1\u201317:29. Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In 31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19-23, 2017, Barcelona, Spain (LIPIcs), Peter M\u00fcller (Ed.), Vol. 74. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 17:1\u201317:29."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_2_2_18_1","volume-title":"POPL","author":"Kokologiannakis Michalis","year":"2018","unstructured":"Michalis Kokologiannakis , Ori Lahav , Konstantinos Sagonas , and Viktor Vafeiadis . 2018. Effective stateless model checking for C\/C++ concurrency. PACMPL 2 , POPL ( 2018 ), 17:1\u201317:32. Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. 2018. Effective stateless model checking for C\/C++ concurrency. PACMPL 2, POPL (2018), 17:1\u201317:32."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.16"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792762"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_36"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12200-2_10"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_54"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837643"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0078-9"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_3_2_2_29_1","volume-title":"Memory ordering in modern microprocessors, part II. Linux Journal 137 (September","author":"McKenney P. E.","year":"2005","unstructured":"P. E. McKenney . September 2005. Memory ordering in modern microprocessors, part II. Linux Journal 137 (September 2005 ). P. E. McKenney. September 2005. Memory ordering in modern microprocessors, part II. Linux Journal 137 (September 2005)."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_3_2_2_31_1","unstructured":"Jarek Nieplocha and Bryan Carpenter. 1999. ARMCI: A Portable Remote Memory Copy Libray for Ditributed Array Libraries and Compiler Run-Time Systems. In Parallel and Distributed Processing 11 IPPS\/SPDP\u201999 Workshops Held in Conjunction with the 13th International Parallel Processing Symposium and 10th Symposium on Parallel and Distributed Processing San Juan Puerto Rico USA April 12-16 1999 Proceedings (Lecture Notes in Computer Science) Vol. 1586. Springer 533\u2013546.   Jarek Nieplocha and Bryan Carpenter. 1999. ARMCI: A Portable Remote Memory Copy Libray for Ditributed Array Libraries and Compiler Run-Time Systems. In Parallel and Distributed Processing 11 IPPS\/SPDP\u201999 Workshops Held in Conjunction with the 13th International Parallel Processing Symposium and 10th Symposium on Parallel and Distributed Processing San Juan Puerto Rico USA April 12-16 1999 Proceedings (Lecture Notes in Computer Science) Vol. 1586. Springer 533\u2013546."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2806886"},{"key":"e_1_3_2_2_34_1","volume-title":"Operational Aspects of C\/C++ Concurrency. CoRR abs\/1606.01400","author":"Podkopaev Anton","year":"2016","unstructured":"Anton Podkopaev , Ilya Sergey , and Aleksandar Nanevski . 2016. Operational Aspects of C\/C++ Concurrency. CoRR abs\/1606.01400 ( 2016 ). arXiv: 1606.01400 http:\/\/arxiv.org\/abs\/1606.01400 Anton Podkopaev, Ilya Sergey, and Aleksandar Nanevski. 2016. Operational Aspects of C\/C++ Concurrency. CoRR abs\/1606.01400 (2016). arXiv: 1606.01400 http:\/\/arxiv.org\/abs\/1606.01400"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1946-08555-9"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_33"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_2_2_39_1","volume-title":"SEFM 2017, Trento, Italy, September 4-8, 2017, Proceedings (Lecture Notes in Computer Science), Alessandro Cimatti and Marjan Sirjani (Eds.)","volume":"10469","author":"Tomasco Ermenegildo","year":"2017","unstructured":"Ermenegildo Tomasco , Truc Lam Nguyen , Bernd Fischer , Salvatore La Torre , and Gennaro Parlato . 2017 . Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models. In Software Engineering and Formal Methods - 15th International Conference , SEFM 2017, Trento, Italy, September 4-8, 2017, Proceedings (Lecture Notes in Computer Science), Alessandro Cimatti and Marjan Sirjani (Eds.) , Vol. 10469 . Springer, 185\u2013202. Ermenegildo Tomasco, Truc Lam Nguyen, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2017. Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models. In Software Engineering and Formal Methods - 15th International Conference, SEFM 2017, Trento, Italy, September 4-8, 2017, Proceedings (Lecture Notes in Computer Science), Alessandro Cimatti and Marjan Sirjani (Eds.), Vol. 10469. Springer, 185\u2013202."},{"key":"e_1_3_2_2_40_1","volume-title":"PTR Prentice Hall","author":"Weaver D.","year":"1994","unstructured":"D. Weaver and T. Germond . PTR Prentice Hall , 1994 . The SPARC Architecture Manual Version 9. D. Weaver and T. Germond. PTR Prentice Hall, 1994. The SPARC Architecture Manual Version 9."}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314649","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314649","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:29Z","timestamp":1750204409000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314649"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":40,"alternative-id":["10.1145\/3314221.3314649","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314649","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}