{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T18:14:01Z","timestamp":1757700841714,"version":"3.40.4"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906428","type":"print"},{"value":"9783031906435","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Analyzing concurrent programs often involves reasoning about happens-before relations, handled by dedicated SMT theory solvers. Recently, preventative propagation rules have been introduced for consistency models to avoid unnecessary computations. This paper analyses the reproducibility of a recently published paper regarding a conflict-avoiding happens-before propagator. We show that the underlying axioms are insufficient for supporting sequential consistency. We find that the algorithm can leave out constraints on event ordering (even considering the original axioms), impacting the accuracy of verification. We show a simple counterexample to the stability claim in the paper. Two revisions of the algorithm are presented, and a proof on the correctness of these approaches respective of the original axioms is shown. The tool implementing the original algorithm is examined to ascertain how it circumvents wrong results. It is found that it deviates from the published algorithm. We show that an unmodified algorithm (via a patch in the implementing tool) causes incorrect results. We also show that our revised algorithm can be implemented efficiently in an independent verification tool.<\/jats:p>","DOI":"10.1007\/978-3-031-90643-5_1","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:08:27Z","timestamp":1745993307000},"page":"3-19","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["On Stability in a Happens-Before Propagator for Concurrent Programs (Reproducibility Study)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6551-5860","authenticated-orcid":false,"given":"Levente","family":"Bajczi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6260-5908","authenticated-orcid":false,"given":"Csan\u00e1d","family":"Telbisz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2912-028X","authenticated-orcid":false,"given":"D\u00e1niel","family":"Szekeres","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7617-3563","authenticated-orcid":false,"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"F.\u00a0He, Z.\u00a0Sun, and H.\u00a0Fan, \u201cDeagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution),\u201d in Tools and Algorithms for the Construction and Analysis of Systems, D.\u00a0Fisman and G.\u00a0Rosu, Eds. Cham: Springer International Publishing, 2022, pp. 424\u2013428.","DOI":"10.1007\/978-3-030-99527-0_25"},{"key":"1_CR2","unstructured":"Z.\u00a0Sun, \u201cDeagle for SV-COMP 2024,\u201d Nov. 2023. [Online]. Available: https:\/\/doi.org\/10.5281\/zenodo.10207348"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"D.\u00a0Beyer, \u201cProgress on Software Verification: SV-COMP 2022,\u201d ser. Lecture Notes in Computer Science, D.\u00a0Fisman and G.\u00a0Rosu, Eds., vol. 13244.\u00a0\u00a0\u00a0Springer, 2022, pp. 375\u2013402. [Online]. Available: https:\/\/doi.org\/10.1007\/978-3-030-99527-0_20","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"D. Beyer, \u201cCompetition on Software Verification and Witness Validation: SV-COMP 2023,\u201d ser. Lecture Notes in Computer Science, S.\u00a0Sankaranarayanan and N.\u00a0Sharygina, Eds., vol. 13994.\u00a0\u00a0\u00a0Springer, 2023, pp. 495\u2013522. [Online]. Available: https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Z.\u00a0Sun, H.\u00a0Fan, and F.\u00a0He, \u201cConsistency-preserving propagation for SMT solving of concurrent program verification,\u201d Proc. ACM Program. Lang., vol.\u00a06, no. OOPSLA2, oct 2022. [Online]. Available: https:\/\/doi.org\/10.1145\/3563321","DOI":"10.1145\/3563321"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"J.\u00a0Alglave, L.\u00a0Maranget, S.\u00a0Sarkar, and P.\u00a0Sewell, \u201cFences in weak memory models (extended version),\u201d Formal Methods Syst. Des., vol.\u00a040, no.\u00a02, pp. 170\u2013205, 2012. [Online]. Available: https:\/\/doi.org\/10.1007\/s10703-011-0135-z","DOI":"10.1007\/s10703-011-0135-z"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"J.\u00a0Alglave, D.\u00a0Kroening, and M.\u00a0Tautschnig, \u201cPartial Orders for Efficient Bounded Model Checking of Concurrent Software,\u201d in Computer Aided Verification, N.\u00a0Sharygina and H.\u00a0Veith, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 141\u2013157.","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"T.\u00a0Haas, R.\u00a0Meyer, and H.\u00a0Ponce\u00a0de Le\u00f3n, \u201cCAAT: consistency as a theory,\u201d Proc. ACM Program. Lang., vol.\u00a06, no. OOPSLA2, oct 2022. [Online]. Available: https:\/\/doi.org\/10.1145\/3563292","DOI":"10.1145\/3563292"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"F.\u00a0He, Z.\u00a0Sun, and H.\u00a0Fan, \u201cSatisfiability modulo ordering consistency theory for multi-threaded program verification,\u201d in Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, ser. PLDI 2021. New York, NY, USA: Association for Computing Machinery, 2021, p. 1264-1279. [Online]. Available: https:\/\/doi.org\/10.1145\/3453483.3454108","DOI":"10.1145\/3453483.3454108"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"H.\u00a0Ponce-de Le\u00f3n, F.\u00a0Furbach, K.\u00a0Heljanko, and R.\u00a0Meyer, \u201cDartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution),\u201d in Tools and Algorithms for the Construction and Analysis of Systems, A.\u00a0Biere and D.\u00a0Parker, Eds. Cham: Springer International Publishing, 2020, pp. 378\u2013382.","DOI":"10.1007\/978-3-030-45237-7_24"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"C.\u00a0Barrett and C.\u00a0Tinelli, Satisfiability Modulo Theories. Cham: Springer International Publishing, 2018, pp. 305\u2013343. [Online]. Available: https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"N.\u00a0Bj\u00f8rner, C.\u00a0Eisenhofer, and L.\u00a0Kov\u00e1cs, \u201cSatisfiability Modulo Custom Theories in Z3,\u201d in Verification, Model Checking, and Abstract Interpretation, C.\u00a0Dragoi, M.\u00a0Emmi, and J.\u00a0Wang, Eds. Cham: Springer Nature Switzerland, 2023, pp. 91\u2013105.","DOI":"10.1007\/978-3-031-24950-1_5"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"C.\u00a0Wang, S.\u00a0Kundu, M.\u00a0Ganai, and A.\u00a0Gupta, \u201cSymbolic Predictive Analysis for Concurrent Programs,\u201d in FM 2009: Formal Methods, A.\u00a0Cavalcanti and D.\u00a0R. Dams, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009, pp. 256\u2013272.","DOI":"10.1007\/978-3-642-05089-3_17"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"R.\u00a0Zennou, M.\u00a0F. Atig, R.\u00a0Biswas, A.\u00a0Bouajjani, C.\u00a0Enea, and M.\u00a0Erradi, \u201cBoosting Sequential Consistency Checking Using Saturation,\u201d in Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, ser. Lecture Notes in Computer Science, D.\u00a0V. Hung and O.\u00a0Sokolsky, Eds., vol. 12302. Springer, 2020, pp. 360\u2013376. [Online]. Available: https:\/\/doi.org\/10.1007\/978-3-030-59152-6_20","DOI":"10.1007\/978-3-030-59152-6_20"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"P.\u00a0B. Gibbons and E.\u00a0Korach, \u201cTesting shared memories,\u201d SIAM Journal on Computing, vol.\u00a026, no.\u00a04, pp. 1208\u20131244, 1997.","DOI":"10.1137\/S0097539794279614"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"T.\u00a0T\u00f3th, A.\u00a0Hajdu, A.\u00a0V\u00f6r\u00f6s et\u00a0al., \u201cTheta: a Framework for Abstraction Refinement-Based Model Checking,\u201d in 17th Conference on Formal Methods in Computer-Aided Design, D.\u00a0Stewart and G.\u00a0Weissenbacher, Eds., 2017, pp. 176\u2013179.","DOI":"10.23919\/FMCAD.2017.8102257"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"D.\u00a0Beyer, S.\u00a0L\u00f6we, and P.\u00a0Wendler, \u201cReliable benchmarking: requirements and solutions,\u201d Int. J. Softw. Tools Technol. Transf., vol.\u00a021, no.\u00a01, pp. 1\u201329, 2019.","DOI":"10.1007\/s10009-017-0469-y"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90643-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:08:32Z","timestamp":1745993312000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90643-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906428","9783031906435"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90643-5_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}