{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:28:18Z","timestamp":1742912898994,"version":"3.40.3"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319522333"},{"type":"electronic","value":"9783319522340"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-52234-0_14","type":"book-chapter","created":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T23:52:06Z","timestamp":1484092326000},"page":"246-265","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Dynamic Reductions for Model Checking Concurrent Software"],"prefix":"10.1007","author":[{"given":"Henning","family":"G\u00fcnther","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alfons","family":"Laarman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ana","family":"Sokolova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,1,12]]},"reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/3-540-63166-6_34","volume-title":"Computer Aided Verification","author":"R Alur","year":"1997","unstructured":"Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-order reduction in symbolic state space exploration. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 340\u2013351. Springer, Heidelberg (1997). doi:\n                    10.1007\/3-540-63166-6_34"},{"key":"14_CR2","unstructured":"Beyer, D.: The software verification competition website. \n                    http:\/\/sv-comp.sosy-lab.org\/2016\/"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"887","DOI":"10.1007\/978-3-662-49674-9_55","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2016","unstructured":"Beyer, D.: Reliable and reproducible competition results with benchexec and witnesses (Report on SV-COMP 2016). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 887\u2013904. Springer, Heidelberg (2016). doi:\n                    10.1007\/978-3-662-49674-9_55"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Erkan Keremoglu, M., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25\u201332. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-540-73368-3_51","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 504\u2013518. Springer, Heidelberg (2007). doi:\n                    10.1007\/978-3-540-73368-3_51"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1007\/978-3-319-08867-9_55","volume-title":"Computer Aided Verification","author":"Johannes Birgmeier","year":"2014","unstructured":"Birgmeier, Johannes, Bradley, Aaron, R., Weissenbacher, Georg: Counterexample to induction-guided abstraction-refinement (CTIGAR). In: Biere, Armin, Bloem, Roderick (eds.) CAV 2014. LNCS, vol. 8559, pp. 831\u2013848. Springer, Cham (2014). doi:\n                    10.1007\/978-3-319-08867-9_55"},{"key":"14_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-349-03521-2","volume-title":"Graph Theory with Applications","author":"JA Bondy","year":"1976","unstructured":"Bondy, J.A., Murty, U.S.R.: Graph Theory with Applications, vol. 290. Macmillan, London (1976)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). doi:\n                    10.1007\/978-3-642-18275-4_7"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-54862-8_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2014","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 46\u201361. Springer, Heidelberg (2014). doi:\n                    10.1007\/978-3-642-54862-8_4"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/BFb0055631","volume-title":"CONCUR\u201998 Concurrency Theory","author":"E Cohen","year":"1998","unstructured":"Cohen, E., Lamport, L.: Reduction in TLA. In: Sangiorgi, D., Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 317\u2013331. Springer, Heidelberg (1998). doi:\n                    10.1007\/BFb0055631"},{"issue":"6","key":"14_CR11","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1145\/2666356.2594322","volume":"49","author":"D Dimitrov","year":"2014","unstructured":"Dimitrov, D., et al.: Commutativity race detection. ACM SIGPLAN Not. 49(6), 305\u2013315 (2014)","journal-title":"ACM SIGPLAN Not."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Doeppner Jr., T.W.: Parallel program correctness through refinement. In: POPL, pp. 155\u2013169. ACM (1977)","DOI":"10.1145\/512950.512965"},{"issue":"2\u20133","key":"14_CR13","first-page":"199","volume":"25","author":"MB Dwyer","year":"2004","unstructured":"Dwyer, M.B., Robby, J.H., Ranganath, V.P.: Exploiting object escape, locking information in partial-order reductions for concurrent object-oriented programs. FMSD 25(2\u20133), 199\u2013240 (2004)","journal-title":"FMSD"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: POPL, pp. 2\u201315. ACM (2009)","DOI":"10.1145\/1594834.1480885"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, vol. 40, no. 1, pp. 110\u2013121. ACM (2005)","DOI":"10.1145\/1047659.1040315"},{"issue":"3","key":"14_CR16","first-page":"518","volume":"89","author":"C Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Transactions for software model checking. ENTCS 89(3), 518\u2013539 (2003). Software Model Checking","journal-title":"ENTCS"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI, pp. 338\u2013349. ACM (2003)","DOI":"10.1145\/780822.781169"},{"key":"14_CR18","unstructured":"G\u00fcnther, H., Laarman, A., Sokolova, A., Weissenbacher, G.: Dynamic reductions for model checking concurrent software (2016). \n                    https:\/\/arxiv.org\/abs\/1611.09318"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","year":"1996","unstructured":"Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-61474-5_79","volume-title":"Computer Aided Verification","author":"EP Gribomont","year":"1996","unstructured":"Gribomont, E.P.: Atomicity refinement and trace reduction theorems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 311\u2013322. Springer, Heidelberg (1996). doi:\n                    10.1007\/3-540-61474-5_79"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Lerda, F., Strichman, O., Theobald, M.: Proof-guided under approximation-widening for multi-process systems. In: POPL, pp. 122\u2013131. ACM (2005)","DOI":"10.1145\/1047659.1040316"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-73370-6_8","volume-title":"Model Checking Software","author":"G Gueta","year":"2007","unstructured":"Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 95\u2013112. Springer, Heidelberg (2007). doi:\n                    10.1007\/978-3-540-73370-6_8"},{"key":"14_CR23","unstructured":"G\u00fcnther, H.: The Vienna verification tool website. \n                    http:\/\/vvt.forsyte.at\/\n                    \n                  . Accessed 21 Nov 2016"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"954","DOI":"10.1007\/978-3-662-49674-9_69","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H G\u00fcnther","year":"2016","unstructured":"G\u00fcnther, H., Laarman, A., Weissenbacher, G.: Vienna verification tool: IC3 for parallel software. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 954\u2013957. Springer, Heidelberg (2016). doi:\n                    10.1007\/978-3-662-49674-9_69"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"G\u00fcnther, H., Weissenbacher, G.: Incremental bounded software model checking. In: SPIN, pp. 40\u201347. ACM (2014)","DOI":"10.1145\/2632362.2632374"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370. ACM (2002)","DOI":"10.1145\/565816.503279"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/11817963_28","volume-title":"Computer Aided Verification","author":"V Kahlon","year":"2006","unstructured":"Kahlon, V., Gupta, A., Sinha, N.: Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 286\u2013299. Springer, Heidelberg (2006). doi:\n                    10.1007\/11817963_28"},{"key":"14_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-02658-4_31","volume-title":"Computer Aided Verification","author":"V Kahlon","year":"2009","unstructured":"Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: an optimal symbolic partial order reduction technique. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 398\u2013413. Springer, Heidelberg (2009). doi:\n                    10.1007\/978-3-642-02658-4_31"},{"key":"14_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/BFb0054182","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Kurshan","year":"1998","unstructured":"Kurshan, R., Levin, V., Minea, M., Peled, D., Yenig\u00fcn, H.: Static partial order reduction. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 345\u2013357. Springer, Heidelberg (1998). doi:\n                    10.1007\/BFb0054182"},{"key":"14_CR30","unstructured":"Laarman, A.W., van de Pol, J.C., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: FMCAD, pp. 247\u2013255. IEEE-CS (2010)"},{"key":"14_CR31","unstructured":"Lamport, L., Schneider, F.B.: Pretending atomicity. Technical report, Cornell University (1989)"},{"issue":"12","key":"14_CR32","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"key":"14_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006). doi:\n                    10.1007\/11817963_14"},{"key":"14_CR34","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, New York (1989)"},{"issue":"3","key":"14_CR35","first-page":"231","volume":"20","author":"R Nalumasu","year":"2002","unstructured":"Nalumasu, R., Gopalakrishnan, G.: An efficient partial order reduction algorithm with an alternative proviso implementation. FMSD 20(3), 231\u2013247 (2002)","journal-title":"FMSD"},{"key":"14_CR36","series-title":"Principles of Computer Science Series","volume-title":"The Theory of Database Concurrency Control","author":"C Papadimitriou","year":"1986","unstructured":"Papadimitriou, C.: The Theory of Database Concurrency Control. Principles of Computer Science Series. Computer Science Press, San Jose (1986)"},{"key":"14_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167\u2013183. Springer, Berlin, Heidelberg (1981). doi:\n                    10.1007\/BFb0017309"},{"key":"14_CR38","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. 697, pp. 409\u2013423. Springer, Heidelberg (1993). doi:\n                    10.1007\/3-540-56922-7_34"},{"key":"14_CR39","doi-asserted-by":"crossref","unstructured":"Popeea, C., Rybalchenko, A., Wilhelm, A.: Reduction for compositional verification of multi-threaded programs. In: FMCAD, pp. 187\u2013194. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987612"},{"key":"14_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/3-540-36577-X_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"SD Stoller","year":"2003","unstructured":"Stoller, S.D., Cohen, E.: Optimistic synchronization-based state-space reduction. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 489\u2013504. Springer, Heidelberg (2003). doi:\n                    10.1007\/3-540-36577-X_36"},{"key":"14_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-51285-3_35","volume-title":"PARLE \u201989 Parallel Architectures and Languages Europe","author":"A Valmari","year":"1989","unstructured":"Valmari, A.: Eliminating redundant interleavings during concurrent program verification. In: Odijk, E., Rem, M., Syre, J.-C. (eds.) PARLE 1989. LNCS, vol. 366, pp. 89\u2013103. Springer, Heidelberg (1989). doi:\n                    10.1007\/3-540-51285-3_35"},{"key":"14_CR42","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.) ICATPN 1989. LNCS, vol. 483, pp. 491\u2013515. Springer, Heidelberg (1991). doi:\n                    10.1007\/3-540-53863-1_36"},{"key":"14_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-78800-3_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Wang","year":"2008","unstructured":"Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 382\u2013396. Springer, Heidelberg (2008). doi:\n                    10.1007\/978-3-540-78800-3_29"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-52234-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T02:10:46Z","timestamp":1558318246000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52234-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522333","9783319522340"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52234-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"12 January 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 January 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/conf.researchr.org\/home\/VMCAI-2017","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}