{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:22:21Z","timestamp":1779074541679,"version":"3.51.4"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816841","type":"print"},{"value":"9783030816858","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thread interleavings, SMC attempts to partition this space into equivalence classes and explore only a few representatives from each class. The efficiency of this approach depends on two factors: (a)\u00a0the coarseness of the partitioning, and (b)\u00a0the time to generate representatives in each class. For this reason, the search for coarse partitionings that are efficiently explorable is an active research challenge.<\/jats:p><jats:p>In this work we present<jats:inline-formula><jats:alternatives><jats:tex-math>$${\\text {RVF-SMC}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mtext>RVF-SMC<\/mml:mtext><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, a new SMC algorithm that uses a novel<jats:italic>reads-value-from (RVF)<\/jats:italic>partitioning. Intuitively, two interleavings are deemed equivalent if they agree on the value obtained in each read event, and read events induce consistent causal orderings between them. The RVF partitioning is provably coarser than recent approaches based on Mazurkiewicz and \u201creads-from\u201d partitionings. Our experimental evaluation reveals that RVF is quite often a very effective equivalence, as the underlying partitioning is exponentially coarser than other approaches. Moreover,<jats:inline-formula><jats:alternatives><jats:tex-math>$${\\text {RVF-SMC}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mtext>RVF-SMC<\/mml:mtext><\/mml:math><\/jats:alternatives><\/jats:inline-formula>generates representatives very efficiently, as the reduction in the partitioning is often met with significant speed-ups in the model checking task.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_16","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"341-366","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Stateless Model Checking Under a Reads-Value-From Equivalence"],"prefix":"10.1007","author":[{"given":"Pratyush","family":"Agarwal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shreya","family":"Pathak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Toman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"16_CR1","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: OSDI (2008)"},{"key":"16_CR2","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: POPL (1997)","DOI":"10.1145\/263699.263717"},{"issue":"2","key":"16_CR4","first-page":"77","volume":"26","author":"P Godefroid","year":"2005","unstructured":"Godefroid, P.: Software model checking: the VeriSoft approach. FMSD 26(2), 77\u2013101 (2005)","journal-title":"FMSD"},{"key":"16_CR5","unstructured":"Ball, T., Musuvathi, M., Qadeer, S.: Chess: a systematic testing tool for concurrent software. Technical report (2007)"},{"key":"16_CR6","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem","author":"P Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, Secaucus (1996)"},{"issue":"6","key":"16_CR7","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1145\/1273442.1250785","volume":"42","author":"M Musuvathi","year":"2007","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. SIGPLAN Not. 42(6), 446\u2013455 (2007)","journal-title":"SIGPLAN Not."},{"issue":"1","key":"16_CR8","first-page":"73","volume":"35","author":"A Lal","year":"2009","unstructured":"Lal, A., Reps, T.: Reducing concurrent analysis under a context bound to sequential analysis. FMSD 35(1), 73\u201397 (2009)","journal-title":"FMSD"},{"key":"16_CR9","unstructured":"Chini, P., Kolberg, J., Krebs, A., Meyer, R., Saivasan, P.: On the complexity of bounded context switching. In: Pruhs, K., Sohler, C. (eds.) 25th Annual European Symposium on Algorithms (ESA 2017), Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, vol. 87, pp. 27:1\u201327:15. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. (2017)"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Baumann, P., Majumdar, R., Thinniyam, R.S., Zetzsche, G.: Context-bounded verification of liveness properties for multithreaded shared-memory programs. In: Proceedings of ACM Programming Language, vol. 5, no. POPL, pp. 1\u201331 (2021)","DOI":"10.1145\/3434325"},{"issue":"3","key":"16_CR11","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s100090050035","volume":"2","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. STTT 2(3), 279\u2013287 (1999)","journal-title":"STTT"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: CAV (1993)","DOI":"10.1007\/3-540-56922-7_34"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/3-540-17906-2_30","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency","author":"A Mazurkiewicz","year":"1987","unstructured":"Mazurkiewicz, A.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 278\u2013324. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-17906-2_30"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL (2005)","DOI":"10.1145\/1040305.1040315"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: POPL (2014)","DOI":"10.1145\/2535838.2535845"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Nguyen, H.T.T., Rodr\u00edguez, C., Sousa, M., Coti, C., Petrucci, L.: Quasi-optimal partial order reduction. In: Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, 14\u201317 July, 2018, Proceedings, Part II, pp. 354\u2013371 (2018)","DOI":"10.1007\/978-3-319-96142-2_22"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Aronis, S., Jonsson, B., L\u00e5ng, M., Sagonas, K.: Optimal dynamic partial order reduction with observers. In: Beyer, D., Huisman, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 229\u2013248. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_14","DOI":"10.1007\/978-3-319-89963-3_14"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Pirottin, D.: Refining dependencies improves partial-order verification methods (extended abstract). In: CAV (1993)","DOI":"10.1007\/3-540-56922-7_36"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/978-3-319-63387-9_26","volume-title":"Computer Aided Verification","author":"E Albert","year":"2017","unstructured":"Albert, E., Arenas, P., de la Banda, M.G., G\u00f3mez-Zamalloa, M., Stuckey, P.J.: Context-sensitive dynamic partial order reduction. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 526\u2013543. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_26"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Raad, A., Vafeiadis, V.: Effective lock handling in stateless model checking. In: Proceedings of ACM Programming Language, vol. 3, no. OOPSLA, pp. 1\u201326 (2019)","DOI":"10.1145\/3360599"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., Vaidya, K.: Data-centric dynamic partial order reduction. In: Proceedings of ACM Programming Language, vol. 2, no. POPL, pp. 31:1\u201331:30 (2017)","DOI":"10.1145\/3158119"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., L\u00e5ng, M., Ngo, T.P., Sagonas, K.: Optimal stateless model checking for reads-from equivalence under sequential consistency. In: Proceedings of ACM Programming Language, vol. 3, no. OOPSLA, pp. 1\u201329 (2019)","DOI":"10.1145\/3360576"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Pavlogiannis, A., Toman, V.: Value-centric dynamic partial order reduction. In: Proceedings of ACM Programming Language, vol. 3, no. OOPSLA, pp. 1\u201329 (2019)","DOI":"10.1145\/3360550"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Huang, J.: Stateless model checking concurrent programs with maximal causality reduction. In: PLDI (2015)","DOI":"10.1145\/2737924.2737975"},{"issue":"4","key":"16_CR25","doi-asserted-by":"publisher","first-page":"1208","DOI":"10.1137\/S0097539794279614","volume":"26","author":"PB Gibbons","year":"1997","unstructured":"Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4), 1208\u20131244 (1997)","journal-title":"SIAM J. Comput."},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Ngo, T.P.: Optimal stateless model checking under the release-acquire semantics. In: Proceedings of ACM Programming Language, vol. 2, no. OOPSLA, pp. 135:1\u2013135:29 (2018)","DOI":"10.1145\/3276505"},{"issue":"8","key":"16_CR27","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1007\/s00236-016-0275-0","volume":"54","author":"PA Abdulla","year":"2016","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. Acta Informatica 54(8), 789\u2013818 (2016). https:\/\/doi.org\/10.1007\/s00236-016-0275-0","journal-title":"Acta Informatica"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Raad, A., Vafeiadis, V.: Model checking for weakly consistent libraries. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, New York, NY, USA, pp. 96\u2013110. ACM (2019)","DOI":"10.1145\/3314221.3314609"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for c\/c++ concurrency. In: Proceedings of ACM Programming Language, 2, no. POPL, pp. 17:1\u201317:32 (2017)","DOI":"10.1145\/3158105"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Agarwal, P., Chatterjee, K., Pathak, S., Pavlogiannis, A., Toman, V.: Stateless model checking under a reads-value-from equivalence. CoRR\/arXiv abs\/2105.06424 (2021)","DOI":"10.1007\/978-3-030-81685-8_16"},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"Pavlogiannis, A.: Fast, sound, and effectively complete dynamic race prediction. In: Proceedings ACM Programming Language, vol. 4, no. POPL, pp. 1\u201329 (2019)","DOI":"10.1145\/3371085"},{"key":"16_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-030-59152-6_21","volume-title":"Automated Technology for Verification and Analysis","author":"M L\u00e5ng","year":"2020","unstructured":"L\u00e5ng, M., Sagonas, K.: Parallel graph-based stateless model checking. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 377\u2013393. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_21"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Norris, B., Demsky, B.: A practical approach for model checking C\/C++11 code. ACM Trans. Program. Lang. Syst. 38(3), 10:1\u201310:51 (2016)","DOI":"10.1145\/2806886"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81685-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,4]],"date-time":"2023-01-04T18:41:41Z","timestamp":1672857701000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"290","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}