{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:36:47Z","timestamp":1791459407439,"version":"4.3.4"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>We present a stateless model checking algorithm for verifying concurrent programs running under RC11, a repaired version of the C\/C++11 memory model without dependency cycles. Unlike most previous approaches, which enumerate thread interleavings up to some partial order reduction improvements, our approach works directly on execution graphs and (in the absence of RMW instructions and SC atomics) avoids redundant exploration by construction. We have implemented a model checker, called RCMC, based on this approach and applied it to a number of challenging concurrent programs. Our experiments confirm that RCMC is significantly faster, scales better than other model checking tools, and is also more resilient to small changes in the benchmarks.<\/jats:p>","DOI":"10.1145\/3158105","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T09:21:49Z","timestamp":1514539309000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":96,"title":["Effective stateless model checking for C\/C++ concurrency"],"prefix":"10.1145","volume":"2","author":[{"given":"Michalis","family":"Kokologiannakis","sequence":"first","affiliation":[{"name":"National Technical University of Athens, Greece"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Konstantinos","family":"Sagonas","sequence":"additional","affiliation":[{"name":"Uppsala University, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3073408"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_8"},{"key":"e_1_2_2_5_1","unstructured":"Jade Alglave. 2013. Weakness is a virtue (position paper). In EC 2 . http:\/\/www0.cs.ucl.ac.uk\/staff\/j.alglave\/papers\/ec213.pdf  Jade Alglave. 2013. Weakness is a virtue (position paper). In EC 2 . http:\/\/www0.cs.ucl.ac.uk\/staff\/j.alglave\/papers\/ec213.pdf"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_28"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958083"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2618128.2618134"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009888"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567080"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814297"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794279614"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1489-x"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737975"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984025"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-014-0150-6"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_25"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17906-2_30"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384314"},{"key":"e_1_2_2_29_1","volume-title":"Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation. USENIX Association","author":"Musuvathi Mandanlal","year":"2008"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2806886"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_22"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.456"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42277"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737956"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158105","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158105","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:11:30Z","timestamp":1750198290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158105"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":37,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158105"],"URL":"https:\/\/doi.org\/10.1145\/3158105","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}