{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:42:48Z","timestamp":1770280968107,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466803","type":"print"},{"value":"9783662466810","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46681-0_28","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T18:56:36Z","timestamp":1427741796000},"page":"353-367","source":"Crossref","is-referenced-by-count":86,"title":["Stateless Model Checking for TSO and PSO"],"prefix":"10.1007","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","reference":[{"key":"28_CR1","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO (2015) arXiv:1501.02069"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: POPL, pp. 373\u2013384. ACM (2014)","DOI":"10.1145\/2535838.2535845"},{"key":"28_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-28756-5_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2012","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Counter-example guided fence insertion under TSO. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 204\u2013219. Springer, Heidelberg (2012)"},{"issue":"12","key":"28_CR4","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S.V. Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. Computer\u00a029(12), 66\u201376 (1996)","journal-title":"Computer"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-642-37036-6_28","volume-title":"Programming Languages and Systems","author":"J. Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 512\u2013532. Springer, Heidelberg (2013)"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-39799-8_9","volume-title":"Computer Aided Verification","author":"J. Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 141\u2013157. Springer, Heidelberg (2013)"},{"key":"28_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-22110-1_6","volume-title":"Computer Aided Verification","author":"J. Alglave","year":"2011","unstructured":"Alglave, J., Maranget, L.: Stability in weak memory models. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 50\u201366. Springer, Heidelberg (2011)"},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-642-37036-6_29","volume-title":"Programming Languages and Systems","author":"A. Bouajjani","year":"2013","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 533\u2013553. Springer, Heidelberg (2013)"},{"key":"28_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\/1273442.1250737"},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-70545-1_12","volume-title":"Computer Aided Verification","author":"S. Burckhardt","year":"2008","unstructured":"Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 107\u2013120. Springer, Heidelberg (2008)"},{"key":"28_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/978-3-642-19835-9_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Burnim","year":"2011","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Sound and complete monitoring of sequential consistency for relaxed memory models. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 11\u201325. Springer, Heidelberg (2011)"},{"key":"28_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":"28_CR13","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s100090050035","volume":"2","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. STTT\u00a02(3), 279\u2013287 (1999)","journal-title":"STTT"},{"key":"28_CR14","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\/1047659.1040315"},{"key":"28_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using VeriSoft. In: POPL, pp. 174\u2013186. ACM (1997)","DOI":"10.1145\/263699.263717"},{"issue":"2","key":"28_CR17","doi-asserted-by":"publisher","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 in System Design\u00a026(2), 77\u2013101 (2005)","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"28_CR18","doi-asserted-by":"publisher","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.\u00a038(2), 130\u2013144 (1996)","journal-title":"J. Parallel Distrib. Comput."},{"key":"28_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-642-12029-9_22","volume-title":"Fundamental Approaches to Software Engineering","author":"S. Lauterburg","year":"2010","unstructured":"Lauterburg, S., Karmani, R.K., Marinov, D., Agha, G.: Evaluating ordering heuristics for dynamic partial-order reduction techniques. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE 2010. LNCS, vol.\u00a06013, pp. 308\u2013322. Springer, Heidelberg (2010)"},{"issue":"8","key":"28_CR20","doi-asserted-by":"publisher","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. Computers\u00a050(8), 824\u2013833 (2001)","journal-title":"IEEE Trans. Computers"},{"issue":"6","key":"28_CR21","doi-asserted-by":"publisher","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.\u00a032(6), 382\u2013403 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"28_CR22","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\/2345156.2254115"},{"key":"28_CR23","unstructured":"The LLVM compiler infrastructure, \n                      \n                        http:\/\/llvm.org"},{"key":"28_CR24","series-title":"Lecture Notes in Computer Science","volume-title":"Advances in Petri Nets 1986. Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986","author":"A. Mazurkiewicz","year":"1987","unstructured":"Mazurkiewicz, A.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol.\u00a0255, Springer, Heidelberg (1987)"},{"key":"28_CR25","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":"28_CR26","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":"28_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all, on model-checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 409\u2013423. Springer, Heidelberg (1993)"},{"key":"28_CR28","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":"28_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-540-70889-6_13","volume-title":"Hardware and Software, Verification and Testing","author":"K. Sen","year":"2007","unstructured":"Sen, K., Agha, G.: A race-detection and flipping algorithm for automated testing of multi-threaded programs. In: Bin, E., Ziv, A., Ur, S. (eds.) HVC 2006. LNCS, vol.\u00a04383, pp. 166\u2013182. Springer, Heidelberg (2007)"},{"issue":"7","key":"28_CR30","doi-asserted-by":"publisher","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. of the ACM\u00a053(7), 89\u201397 (2010)","journal-title":"Comm. of the ACM"},{"issue":"2","key":"28_CR31","doi-asserted-by":"publisher","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. on Programming Languages and Systems\u00a010(2), 282\u2013312 (1988)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"28_CR32","unstructured":"SPARC International, Inc. The SPARC Architecture Manual Version 9 (1994)"},{"key":"28_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-30793-5_14","volume-title":"Formal Techniques for Distributed Systems","author":"S. Tasharofi","year":"2012","unstructured":"Tasharofi, S., Karmani, R.K., Lauterburg, S., Legay, A., Marinov, D., Agha, G.: TransDPOR: A novel dynamic partial-order reduction technique for testing actor programs. In: Giese, H., Rosu, G. (eds.) FORTE 2012 and FMOODS 2012. LNCS, vol.\u00a07273, pp. 219\u2013234. Springer, Heidelberg (2012)"},{"key":"28_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/3-540-53863-1_36","volume-title":"Advances in Petri Nets 1990","author":"A. Valmari","year":"1991","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) APN 1990. LNCS, vol.\u00a0483, pp. 491\u2013515. Springer, Heidelberg (1991)"},{"key":"28_CR35","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":"28_CR36","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)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46681-0_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:12:14Z","timestamp":1559139134000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46681-0_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466803","9783662466810"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46681-0_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}