{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:49:20Z","timestamp":1770274160992,"version":"3.49.0"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"8","license":[{"start":{"date-parts":[[2016,7,7]],"date-time":"2016-07-07T00:00:00Z","timestamp":1467849600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100004359","name":"Swedish Research Council","doi-asserted-by":"crossref","award":["621-2014-5489"],"award-info":[{"award-number":["621-2014-5489"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004359","name":"Swedish Research Council","doi-asserted-by":"crossref","award":["70872503"],"award-info":[{"award-number":["70872503"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"crossref"}]},{"name":"EU FP7","award":["287510"],"award-info":[{"award-number":["287510"]}]},{"DOI":"10.13039\/501100004359","name":"Swedish Research Council","doi-asserted-by":"crossref","award":["621-2014-5489"],"award-info":[{"award-number":["621-2014-5489"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004359","name":"Swedish Research Council","doi-asserted-by":"crossref","award":["621-2014-5489"],"award-info":[{"award-number":["621-2014-5489"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1007\/s00236-016-0275-0","type":"journal-article","created":{"date-parts":[[2016,7,7]],"date-time":"2016-07-07T17:26:19Z","timestamp":1467912379000},"page":"789-818","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":35,"title":["Stateless model checking for TSO and PSO"],"prefix":"10.1007","volume":"54","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Stavros","family":"Aronis","sequence":"additional","affiliation":[]},{"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[]},{"given":"Carl","family":"Leonardsson","sequence":"additional","affiliation":[]},{"given":"Konstantinos","family":"Sagonas","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,7,7]]},"reference":[{"key":"275_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: POPL, pp. 373\u2013384. ACM (2014)","DOI":"10.1145\/2535838.2535845"},{"key":"275_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Tools and algorithms for the construction and analysis of systems, pp. 353\u2013367. Springer, Heidelberg (2015)","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"275_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Counter-example guided fence insertion under TSO. In: TACAS, vol. 7214 of LNCS, pp. 204\u2013219. Springer (2012)","DOI":"10.1007\/978-3-642-28756-5_15"},{"issue":"12","key":"275_CR4","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"SV Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: a tutorial. Computer 29(12), 66\u201376 (1996)","journal-title":"Computer"},{"key":"275_CR5","doi-asserted-by":"crossref","unstructured":"Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: ESOP, vol. 7792 of LNCS, pp. 512\u2013532. Springer (2013)","DOI":"10.1007\/978-3-642-37036-6_28"},{"key":"275_CR6","doi-asserted-by":"crossref","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: CAV, vol. 8044 of LNCS, pp. 141\u2013157. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"275_CR7","doi-asserted-by":"crossref","unstructured":"Alglave, J., Maranget, L.: Stability in weak memory models. In: CAV, vol. 6806 of LNCS, pp. 50\u201366. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_6"},{"key":"275_CR8","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: ESOP, vol. 7792 of LNCS, pp. 533\u2013553. Springer (2013)","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"275_CR9","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: CheckFence: checking consistency of concurrent data types on relaxed memory models. In: PLDI, pp. 12\u201321. ACM (2007)","DOI":"10.1145\/1250734.1250737"},{"key":"275_CR10","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: CAV, vol. 5123 of LNCS, pp. 107\u2013120. Springer (2008)","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"275_CR11","doi-asserted-by":"crossref","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Sound and complete monitoring of sequential consistency for relaxed memory models. In: TACAS, pp. 11\u201325. LNCS 6605, Springer (2011)","DOI":"10.1007\/978-3-642-19835-9_3"},{"key":"275_CR12","doi-asserted-by":"crossref","unstructured":"Christakis, M., Gotovos, A., Sagonas, K.: Systematic testing for detecting concurrency errors in Erlang programs. In: ICST, pp. 154\u2013163. IEEE (2013)","DOI":"10.1109\/ICST.2013.50"},{"issue":"3","key":"275_CR13","doi-asserted-by":"crossref","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":"275_CR14","doi-asserted-by":"crossref","unstructured":"Demsky, B., Lam, P.: SATCheck: SAT-directed stateless model checking for SC and TSO. In: OOPSLA (2015)","DOI":"10.1145\/2814270.2814297"},{"key":"275_CR15","volume-title":"Cooperating sequential processes","author":"EW Dijkstra","year":"2002","unstructured":"Dijkstra, E.W.: Cooperating sequential processes. Springer, Heidelberg (2002)"},{"key":"275_CR16","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, pp. 110\u2013121. ACM (2005)","DOI":"10.1145\/1040305.1040315"},{"key":"275_CR17","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems\u2014An Approach to the State-Explosion Problem, vol. 1032 of LNCS. Springer (1996)","DOI":"10.1007\/3-540-60761-7"},{"key":"275_CR18","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: POPL, pp. 174\u2013186. ACM Press (1997)","DOI":"10.1145\/263699.263717"},{"issue":"2","key":"275_CR19","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/s10703-005-1489-x","volume":"26","author":"P Godefroid","year":"2005","unstructured":"Godefroid, P.: Software model checking: the VeriSoft approach. Formal Methods Syst. Des. 26(2), 77\u2013101 (2005)","journal-title":"Formal Methods Syst. Des."},{"key":"275_CR20","doi-asserted-by":"crossref","unstructured":"Huang, J.: Stateless model checking concurrent programs with maximal causality reduction. In: PLDI, pp. 165\u2013174. New York, NY, USA, ACM (2015)","DOI":"10.1145\/2737924.2737975"},{"issue":"2","key":"275_CR21","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1006\/jpdc.1996.0136","volume":"38","author":"A Krishnamurthy","year":"1996","unstructured":"Krishnamurthy, A., Yelick, K.A.: Analyses and optimizations for shared address space programs. J. Parallel Distrib. Comput. 38(2), 130\u2013144 (1996)","journal-title":"J. Parallel Distrib. Comput."},{"key":"275_CR22","doi-asserted-by":"crossref","unstructured":"Lauterburg, S., Karmani, R., Marinov, D., Agha, G.: Evaluating ordering heuristics for dynamic partial-order reduction techniques. In: FASE, pp 308\u2013322. LNCS 6013 (2010)","DOI":"10.1007\/978-3-642-12029-9_22"},{"issue":"8","key":"275_CR23","doi-asserted-by":"crossref","first-page":"824","DOI":"10.1109\/12.947002","volume":"50","author":"J Lee","year":"2001","unstructured":"Lee, J., Padua, D.A.: Hiding relaxed memory consistency with a compiler. IEEE Trans. Comput. 50(8), 824\u2013833 (2001)","journal-title":"IEEE Trans. Comput."},{"issue":"6","key":"275_CR24","doi-asserted-by":"crossref","first-page":"382","DOI":"10.1109\/TSE.2006.56","volume":"32","author":"Y Lei","year":"2006","unstructured":"Lei, Y., Carver, R.: Reachability testing of concurrent programs. IEEE Trans. Softw. Eng. 32(6), 382\u2013403 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"275_CR25","doi-asserted-by":"crossref","unstructured":"Liu, F., Nedev, N., Prisadnikov, N., Vechev, M.T., Yahav, E.: Dynamic synthesis for relaxed memory models. In: PLDI, pp. 429\u2013440. ACM (2012)","DOI":"10.1145\/2254064.2254115"},{"key":"275_CR26","unstructured":"The LLVM compiler infrastructure. http:\/\/llvm.org"},{"key":"275_CR27","doi-asserted-by":"crossref","unstructured":"Mazurkiewicz, A.: Trace theory. In: Advances in Petri Nets (1986)","DOI":"10.1007\/3-540-17906-2_30"},{"key":"275_CR28","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: OSDI, pp. 267\u2013280. USENIX (2008)"},{"key":"275_CR29","doi-asserted-by":"crossref","unstructured":"Park, S., Dill, D.L: An executable specification, analyzer and verifier for RMO (relaxed memory order). In: SPAA, pp. 34\u201341. ACM (1995)","DOI":"10.1145\/215399.215413"},{"key":"275_CR30","doi-asserted-by":"crossref","unstructured":"Peled, D.: All from one, one for all, on model-checking using representatives. In: CAV, vol. 697 of LNCS, pp. 409\u2013423. Springer (1993)","DOI":"10.1007\/3-540-56922-7_34"},{"issue":"3","key":"275_CR31","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G Peterson","year":"1981","unstructured":"Peterson, G., Stickel, M.: Myths about the mutal exclusion problem. Inf. Process. Lett. 12(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"key":"275_CR32","doi-asserted-by":"crossref","unstructured":"Saarikivi, O., K\u00e4hk\u00f6nen, K., Heljanko, K.: Improving dynamic partial order reductions for concolic testing. In: ACSD, IEEE (2012)","DOI":"10.1109\/ACSD.2012.18"},{"key":"275_CR33","doi-asserted-by":"crossref","unstructured":"Sen, K., Agha, G.: A race-detection and flipping algorithm for automated testing of multi-threaded programs. In: Haifa Verification Conference, pp. 166\u2013182. LNCS 4383 (2007)","DOI":"10.1007\/978-3-540-70889-6_13"},{"issue":"7","key":"275_CR34","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P Sewell","year":"2010","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Comm. ACM 53(7), 89\u201397 (2010)","journal-title":"Comm. ACM"},{"issue":"2","key":"275_CR35","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1145\/42190.42277","volume":"10","author":"D Shasha","year":"1988","unstructured":"Shasha, D., Snir, M.: Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst. 10(2), 282\u2013312 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"275_CR36","unstructured":"SPARC International, Inc. The SPARC Architecture Manual Version 9, (1994)"},{"key":"275_CR37","doi-asserted-by":"crossref","unstructured":"Tasharofi, S. et\u00a0al.: TransDPOR: A novel dynamic partial-order reduction technique for testing actor programs. In: FMOODS\/FORTE, pp. 219\u2013234. LNCS 7273 (2012)","DOI":"10.1007\/978-3-642-30793-5_14"},{"key":"275_CR38","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Advances in Petri Nets, vol. 483 of LNCS, pp. 491\u2013515. Springer (1989)","DOI":"10.1007\/3-540-53863-1_36"},{"key":"275_CR39","doi-asserted-by":"crossref","unstructured":"Wang, C., Said, M., Gupta, A.: Coverage guided systematic concurrency testing. In: ICSE, pp. 221\u2013230. ACM (2011)","DOI":"10.1145\/1985793.1985824"},{"key":"275_CR40","doi-asserted-by":"crossref","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Nemos: A framework for axiomatic and executable specifications of memory consistency models. In: IPDPS, IEEE (2004)","DOI":"10.1109\/IPDPS.2004.1302944"},{"key":"275_CR41","doi-asserted-by":"crossref","unstructured":"Zhang, N., Kusano, M., Wang, C.: Dynamic partial order reduction for relaxed memory models. In: Proceedings of the 36th ACM SIGPLAN conference on programming language design and implementation, pp. 250\u2013259. ACM (2015)","DOI":"10.1145\/2737924.2737956"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-016-0275-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0275-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0275-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0275-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,10]],"date-time":"2019-09-10T17:33:23Z","timestamp":1568136803000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-016-0275-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7,7]]},"references-count":41,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2017,12]]}},"alternative-id":["275"],"URL":"https:\/\/doi.org\/10.1007\/s00236-016-0275-0","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,7,7]]}}}