{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T20:19:26Z","timestamp":1743106766589,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319489889"},{"type":"electronic","value":"9783319489896"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-48989-6_23","type":"book-chapter","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T01:31:19Z","timestamp":1478482279000},"page":"370-387","source":"Crossref","is-referenced-by-count":3,"title":["Error Invariants for Concurrent Traces"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Holzer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Schwartz-Narbonne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mitra","family":"Tabaei Befrouei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,8]]},"reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"951","DOI":"10.1007\/978-3-642-39799-8_68","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2013","unstructured":"\u010cern\u00fd, P., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Tarrach, T.: Efficient synthesis for concurrency by semantics-preserving transformations. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 951\u2013967. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_68"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-642-35873-9_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Christ","year":"2013","unstructured":"Christ, J., Ermis, E., Sch\u00e4f, M., Wies, T.: Flow-sensitive fault localization. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 189\u2013208. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-35873-9_13"},{"issue":"4","key":"23_CR3","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Kenneth-Zadeck, F.: Efficiently computing static single assignment form, the control dependence graph. ACM Trans. Program. Lang. Syst. (TOPLAS) 13(4), 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-11319-2_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V D\u2019Silva","year":"2010","unstructured":"D\u2019Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 129\u2013145. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-11319-2_12"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Engler, D.R., Ashcraft, K., RacerX: effective, static detection of race conditions and deadlocks. In: SOSP, pp. 237\u2013252. ACM (2003)","DOI":"10.1145\/1165389.945468"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-32759-9_17","volume-title":"FM 2012: Formal Methods","author":"E Ermis","year":"2012","unstructured":"Ermis, E., Sch\u00e4f, M., Wies, T.: Error invariants. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 187\u2013201. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-32759-9_17"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Farzan, A., Holzer, A., Razavi, N., Veith, H.: Con2colic testing. In: Foundations of Software Engineering (FSE), pp. 37\u201347. ACM (2013)","DOI":"10.1145\/2491411.2491453"},{"issue":"11","key":"23_CR8","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/1839676.1839699","volume":"53","author":"C Flanagan","year":"2010","unstructured":"Flanagan, C., Freund, S.N.: FastTrack: efficient and precise dynamic race detection. Commun. ACM 53(11), 93\u2013101 (2010)","journal-title":"Commun. ACM"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: Programming Language Design and Implementation (PLDI), pp. 338\u2013349. ACM (2003)","DOI":"10.1145\/781131.781169"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Gupta, A., Henzinger, T.A., Radhakrishna, A., Samanta, R., Tarrach, T.: Succinct representation of concurrent trace sets. In: POPL, pp. 433\u2013444. ACM (2015)","DOI":"10.1145\/2676726.2677008"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Holzer, A., Schwartz-Narbonne, D., Tabaei Befrouei, M., Weissenbacher, G., Wies, T.: Error invariants for concurrent traces. ArXiv e-prints, abs\/1608.08584, August 2016","DOI":"10.1007\/978-3-319-48989-6_23"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-23702-7_15","volume-title":"Static Analysis","author":"J Huang","year":"2011","unstructured":"Huang, J., Zhang, C.: An efficient static trace simplification technique for debugging concurrent programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 163\u2013179. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-23702-7_15"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Jalbert, N., Sen, K.: A trace simplification technique for effective debugging of concurrent programs. In: Foundations of Software Engineering (FSE), pp. 57\u201366. ACM (2010)","DOI":"10.1145\/1882291.1882302"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Jin, G., Song, L., Zhang, W., Lu, S., Liblit, B.: Automated atomicity-violation fixing. In: Programming Language Design and Implementation (PLDI), pp. 389\u2013400. ACM (2011)","DOI":"10.1145\/1993498.1993544"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: Programming Language Design and Implementation (PLDI) (2011)","DOI":"10.1145\/1993498.1993550"},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-70545-1_47","volume-title":"Computer Aided Verification","author":"S Kashyap","year":"2008","unstructured":"Kashyap, S., Garg, V.K.: Producing short counterexamples using \u201cCrucial Events\u201d. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 491\u2013503. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-70545-1_47"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Khoshnood, S., Kusano, M., Wang, C., ConcBugAssist: constraint solving for diagnosis and repair of concurrency bugs. In: ISSTA, pp. 165\u2013176. ACM (2015)","DOI":"10.1145\/2771783.2771798"},{"key":"23_CR18","first-page":"329","volume":"43","author":"L Shan","year":"2008","unstructured":"Shan, L., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. ACM SIGPLAN Not. 43, 329\u2013339 (2008)","journal-title":"ACM SIGPLAN Not."},{"issue":"1","key":"23_CR19","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theoret. Comput. Sci. 345(1), 101\u2013121 (2005)","journal-title":"Theoret. Comput. Sci."},{"key":"23_CR20","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: 10.1007\/11817963_14"},{"key":"23_CR21","volume-title":"Advanced Compiler Design Implementation","author":"SS Muchnick","year":"1997","unstructured":"Muchnick, S.S.: Advanced Compiler Design Implementation. Morgan Kaufmann, San Francisco (1997)"},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"Murali, V., Sinha, N., Torlak, E., Chandra, S.: A hybrid algorithm for error trace explanation. In: VSTTE (2014)","DOI":"10.1007\/978-3-319-12154-3_17"},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"Park, S., Vuduc, R., Harrold, M.J.: A unified approach for localizing non-deadlock concurrency bugs. In: Software Testing, Verification and Validation (ICST), pp. 51\u201360. IEEE (2012)","DOI":"10.1109\/ICST.2012.85"},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"Park, S., Vuduc, R.W., Harrold, M.J.: Falcon: fault localization in concurrent programs. In: International Conference on Software Engineering (ICSE), pp. 245\u2013254. ACM (2010)","DOI":"10.1145\/1806799.1806838"},{"issue":"4","key":"23_CR25","doi-asserted-by":"crossref","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.E.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. 15(4), 391\u2013411 (1997)","journal-title":"ACM Trans. Comput. Syst."},{"key":"23_CR26","doi-asserted-by":"crossref","unstructured":"Sinha, N., Wang, C.: On interference abstractions. In: Principles of Programming Languages (POPL), pp. 423\u2013434. ACM (2011)","DOI":"10.1145\/1926385.1926433"},{"key":"23_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-319-11164-3_14","volume-title":"Runtime Verification","author":"M Tabaei Befrouei","year":"2014","unstructured":"Tabaei Befrouei, M., Wang, C., Weissenbacher, G.: Abstraction and mining of traces to explain concurrency bugs. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 162\u2013177. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-11164-3_14"},{"key":"23_CR28","first-page":"121","volume":"3","author":"F Tip","year":"1995","unstructured":"Tip, F.: A survey of program slicing techniques. J. Program. Lang. 3, 121\u2013189 (1995)","journal-title":"J. Program. Lang."},{"issue":"6","key":"23_CR29","doi-asserted-by":"crossref","first-page":"781","DOI":"10.1007\/s00165-011-0179-2","volume":"23","author":"C Wang","year":"2011","unstructured":"Wang, C., Kundu, S., Limaye, R., Ganai, M., Gupta, A.: Symbolic predictive analysis for concurrent programs. Formal Aspects Comput. 23(6), 781\u2013805 (2011)","journal-title":"Formal Aspects Comput."},{"key":"23_CR30","doi-asserted-by":"crossref","unstructured":"Xu, M., Bod\u00edk, R., Hill, M.D.: A serializability violation detector for shared-memory server programs. In: Programming Language Design and Implementation (PLDI), pp. 1\u201314. ACM (2005)","DOI":"10.1145\/1065010.1065013"}],"container-title":["Lecture Notes in Computer Science","FM 2016: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48989-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,15]],"date-time":"2019-09-15T05:54:14Z","timestamp":1568526854000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48989-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319489889","9783319489896"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48989-6_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}