{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:26:00Z","timestamp":1740122760799,"version":"3.37.3"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2016,1,4]],"date-time":"2016-01-04T00:00:00Z","timestamp":1451865600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2016,1,4]],"date-time":"2016-01-04T00:00:00Z","timestamp":1451865600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11403-N23"],"award-info":[{"award-number":["S11403-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1149454"],"award-info":[{"award-number":["CCF-1149454"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2016,10]]},"DOI":"10.1007\/s10703-015-0240-5","type":"journal-article","created":{"date-parts":[[2016,1,4]],"date-time":"2016-01-04T16:26:39Z","timestamp":1451924799000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Abstraction and mining of traces to explain concurrency bugs"],"prefix":"10.1007","volume":"49","author":[{"given":"Mitra","family":"Tabaei\u00a0Befrouei","sequence":"first","affiliation":[]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,1,4]]},"reference":[{"key":"240_CR1","unstructured":"http:\/\/bzip2smp.sourceforge.net\/\n                    \n                  , (bzip2smp 1.0). Accessed in Sept 2015"},{"key":"240_CR2","first-page":"154","volume":"1855","author":"EM Clarke","year":"2000","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. CAV, LNCS 1855:154\u2013169","journal-title":"CAV, LNCS"},{"issue":"12","key":"240_CR3","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1109\/TSE.2004.91","volume":"30","author":"N Delgado","year":"2004","unstructured":"Delgado N, Gates AQ, Roach S (2004) A taxonomy and catalog of runtime software-fault monitoring tools. IEEE Trans Softw Eng (TSE) 30(12):859\u2013872","journal-title":"IEEE Trans Softw Eng (TSE)"},{"issue":"11","key":"240_CR4","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1145\/1839676.1839698","volume":"53","author":"T Elmas","year":"2010","unstructured":"Elmas T, Qadeer S, Tasiran S (2010) Goldilocks: a race-aware Java runtime. Commun ACM 53(11):85\u201392","journal-title":"Commun ACM"},{"key":"240_CR5","unstructured":"Engler DR, Ashcraft K (2003) RacerX: effective, static detection of race conditions and deadlocks. In: Symposium on operating systems principles (SOSP), ACM 2003, pp 237\u2013252"},{"key":"240_CR6","unstructured":"Erickson J, Musuvathi M, Burckhardt S, Olynyk K. (2010) Effective data-race detection for the kernel. In: USENIX symposium on operating systems design and implementation (OSDI), USENIX Association 2010, pp 151\u2013162"},{"issue":"11","key":"240_CR7","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/1839676.1839699","volume":"53","author":"C Flanagan","year":"2010","unstructured":"Flanagan C, Freund SN (2010) FastTrack: efficient and precise dynamic race detection. Commun ACM 53(11):93\u2013101","journal-title":"Commun ACM"},{"key":"240_CR8","doi-asserted-by":"crossref","unstructured":"Flanagan C, Qadeer S (2003) A type and effect system for atomicity. In: PLDI, ACM 2003, pp 338\u2013349","DOI":"10.1145\/781131.781169"},{"key":"240_CR9","doi-asserted-by":"crossref","unstructured":"Fleming SD, Kraemer E, Stirewalt REK, Xie S, Dillon LK (2008) A study of student strategies for the corrective maintenance of concurrent software. In: International conference on software engineering (ICSE), ACM 2008, pp 759\u2013768","DOI":"10.1145\/1368088.1368195"},{"key":"240_CR10","doi-asserted-by":"crossref","unstructured":"Hammer C, Dolby J, Vaziri M, Tip F (2008) Dynamic detection of atomic-set-serializability violations. In: International conference on software engineering (ICSE), ACM 2008, pp 231\u2013240","DOI":"10.1145\/1368088.1368120"},{"key":"240_CR11","volume-title":"The art of multiprocessor programming","author":"M Herlihy","year":"2008","unstructured":"Herlihy M, Shavit N (2008) The art of multiprocessor programming. Morgan Kaufmann, Burlington"},{"issue":"4","key":"240_CR12","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1109\/TC.1987.1676929","volume":"36","author":"TJ LeBlanc","year":"1987","unstructured":"LeBlanc TJ, Mellor-Crummey JM (1987) Debugging parallel programs with instant replay. IEEE Trans Comput 36(4):471\u2013482","journal-title":"IEEE Trans Comput"},{"key":"240_CR13","doi-asserted-by":"crossref","unstructured":"Leue S, Tabaei-Befrouei M (2012) Counterexample explanation by anomaly detection. In: Model checking and software verification (SPIN), 2012","DOI":"10.1007\/978-3-642-31759-0_5"},{"key":"240_CR14","doi-asserted-by":"crossref","unstructured":"Leue S, Tabaei-Befrouei M (2013) Mining sequential patterns to explain concurrent counterexamples. In: Model checking and software verification (SPIN), 2013","DOI":"10.1007\/978-3-642-39176-7_17"},{"key":"240_CR15","volume-title":"Counterfactuals","author":"D Lewis","year":"2001","unstructured":"Lewis D (2001) Counterfactuals. Wiley-Blackwell, New York"},{"key":"240_CR16","unstructured":"Lu S, Jiang W, Zhou Y (2007) A study of interleaving coverage criteria. In: Foundations of software engineering (FSE), ESEC-FSE Companion, ACM 2007, pp 533\u2013536"},{"key":"240_CR17","doi-asserted-by":"crossref","unstructured":"Lu S, Park S, Seo E, Zhou Y (2008) Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: ACM Sigplan Notices, ACM 2008, vol 43, pp 329\u2013339","DOI":"10.1145\/1346281.1346323"},{"key":"240_CR18","doi-asserted-by":"crossref","unstructured":"Lu S, Tucek J, Qin F, Zhou Y (2006) AVIO: detecting atomicity violations via access interleaving invariants. In: Architectural support for programming languages and operating systems (ASPLOS), 2006","DOI":"10.1145\/1168857.1168864"},{"key":"240_CR19","doi-asserted-by":"crossref","unstructured":"Lucia B, Ceze L (2009) Finding concurrency bugs with context-aware communication graphs. In: Symposium on microarchitecture (MICRO), ACM 2009, pp 553\u2013563","DOI":"10.1145\/1669112.1669181"},{"issue":"1","key":"240_CR20","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/1824795.1824798","volume":"43","author":"NR Mabroukeh","year":"2010","unstructured":"Mabroukeh NR, Ezeife CI (2010) A taxonomy of sequential pattern mining algorithms. ACM Comput Surv 43(1):3:1\u20133:41. doi:\n                    10.1145\/1824795.1824798","journal-title":"ACM Comput Surv"},{"key":"240_CR21","unstructured":"Mazurkiewicz AW (1986) Trace theory. In: Petri nets: central models and their properties, advances in petri nets, LNCS, Springer, vol 255, pp 279\u2013324"},{"key":"240_CR22","unstructured":"Musuvathi M, Qadeer S (2006) CHESS: systematic stress testing of concurrent software. In: Logic-based program synthesis and transformation (LOPSTR), LNCS, Springer, vol 4407, pp 15\u201316"},{"key":"240_CR23","doi-asserted-by":"publisher","unstructured":"Musuvathi M, Qadeer S (2007) Iterative context bounding for systematic testing of multithreaded programs. In: PLDI, ACM 2007, pp 446\u2013455. doi:\n                    10.1145\/1250734.1250785","DOI":"10.1145\/1250734.1250785"},{"key":"240_CR24","unstructured":"Musuvathi M, Qadeer S, Ball T (2007) CHESS: a systematic testing tool for concurrent software. Tech Rep MSR-TR-2007-149, Microsoft Research, 2007"},{"issue":"7","key":"240_CR25","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/109626.109640","volume":"26","author":"RHB Netzer","year":"1991","unstructured":"Netzer RHB, Miller BP (1991) Improving the accuracy of data race detection. SIGPLAN Notices 26(7):133\u2013144. doi:\n                    10.1145\/109626.109640","journal-title":"SIGPLAN Notices"},{"issue":"4","key":"240_CR26","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1145\/322154.322158","volume":"26","author":"CH Papadimitriou","year":"1979","unstructured":"Papadimitriou CH (1979) The serializability of concurrent database updates. J ACM 26(4):631\u2013653","journal-title":"J ACM"},{"key":"240_CR27","doi-asserted-by":"crossref","unstructured":"Park S, Lu S, Zhou Y (2009) CTrigger: exposing atomicity violation bugs from their hiding places. In: Architectural support for programming languages and operating systems (ASPLOS), ACM, 2009, pp 25\u201336","DOI":"10.1145\/1508244.1508249"},{"key":"240_CR28","doi-asserted-by":"crossref","unstructured":"Park S, Vuduc R, Harrold MJ (2012) A unified approach for localizing non-deadlock concurrency bugs. In: Software testing, verification and validation (ICST), IEEE 2012, pp 51\u201360","DOI":"10.1109\/ICST.2012.85"},{"key":"240_CR29","doi-asserted-by":"crossref","unstructured":"Park S, Vuduc RW, Harrold MJ (2010) Falcon: fault localization in concurrent programs. In: International conference on software engineering (ICSE), ACM 2010, pp 245\u2013254","DOI":"10.1145\/1806799.1806838"},{"key":"240_CR30","unstructured":"Pei J, Han J, Mortazavi-Asl B, Pinto H, Chen Q, Dayal U, Hsu M (2001) PrefixSpan: Mining sequential patterns efficiently by prefix-projected pattern growth. In: 17th international conference on data engineering (ICDE\u201901), 2001"},{"key":"240_CR31","unstructured":"R\u00f6\u00dfler J, Fraser G, Zeller A, Orso A (2012) Isolating failure causes through test case generation. In: International symposium on software testing and analysis, ACM 2012, pp 309\u2013319"},{"issue":"4","key":"240_CR32","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S Savage","year":"1997","unstructured":"Savage S, Burrows M, Nelson G, Sobalvarro P, Anderson T (1997) Eraser: a dynamic data race detector for multithreaded programs. Trans Comput Syst (TOCS) 15(4):391\u2013411. doi:\n                    10.1145\/265924.265927","journal-title":"Trans Comput Syst (TOCS)"},{"key":"240_CR33","doi-asserted-by":"crossref","unstructured":"Tabaei-Befrouei M, Wang C, Weissenbacher G (2014) Abstraction and mining of traces to explain concurrency bugs. In: Proceedings of the 14th international conference on runtime verification (RV), 2014","DOI":"10.1007\/978-3-319-11164-3_14"},{"key":"240_CR34","doi-asserted-by":"crossref","unstructured":"Wang J, Han J (2004) Bide: efficient mining of frequent closed sequences. In: ICDE, 2004","DOI":"10.1109\/ICDE.2004.1319986"},{"issue":"2","key":"240_CR35","first-page":"93","volume":"32","author":"L Wang","year":"2006","unstructured":"Wang L, Stoller SD (2006) Runtime analysis of atomicity for multithreaded programs. TSE 32(2):93\u2013110","journal-title":"TSE"},{"key":"240_CR36","doi-asserted-by":"crossref","unstructured":"Xu M, Bod\u00edk R, Hill MD (2005) A serializability violation detector for shared-memory server programs. In: PLDI, ACM 2005, pp 1\u201314","DOI":"10.1145\/1065010.1065013"},{"key":"240_CR37","doi-asserted-by":"crossref","unstructured":"Yan X, Han J, Afshar R (2003) CloSpan: mining closed sequential patterns in large datasets. In: Proceedings of 2003 SIAM international conference on data mining (SDM\u201903), 2003","DOI":"10.1137\/1.9781611972733.15"},{"key":"240_CR38","doi-asserted-by":"crossref","unstructured":"Yang Y, Chen X, Gopalakrishnan G, Kirby RM (2007) Distributed dynamic partial order reduction based verification of threaded software. In: Model checking and software verification (SPIN), LNCS 2007, pp 58\u201375","DOI":"10.1007\/978-3-540-73370-6_6"},{"key":"240_CR39","volume-title":"Why Programs Fail: A Guide to Systematic Debugging","author":"A Zeller","year":"2009","unstructured":"Zeller A (2009) Why Programs Fail: A Guide to Systematic Debugging. Morgan Kaufmann, Burlington"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0240-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-015-0240-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0240-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-015-0240-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T15:44:42Z","timestamp":1589730282000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-015-0240-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,4]]},"references-count":39,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["240"],"URL":"https:\/\/doi.org\/10.1007\/s10703-015-0240-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2016,1,4]]},"assertion":[{"value":"4 January 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}