{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:04:19Z","timestamp":1776305059756,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642341878","type":"print"},{"value":"9783642341885","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012]]},"DOI":"10.1007\/978-3-642-34188-5_11","type":"book-chapter","created":{"date-parts":[[2012,10,11]],"date-time":"2012-10-11T14:04:33Z","timestamp":1349964273000},"page":"95-114","source":"Crossref","is-referenced-by-count":12,"title":["Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search"],"prefix":"10.1007","author":[{"given":"Arnab","family":"Sinha","sequence":"first","affiliation":[]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"key":"11_CR2","unstructured":"Z3: Linux binary, \n                    \n                      http:\/\/research.microsoft.com\/enus\/um\/redmond\/projects\/z3\/download.html"},{"key":"11_CR3","unstructured":"Farchi, E., Nir, Y., Ur, S.: Concurrent Bug Patterns and How to Test Them. In: IPDPS, p. 286 (2003)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/11817963_30","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2006","unstructured":"Farzan, A., Madhusudan, P.: Causal Atomicity. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 315\u2013328. Springer, Heidelberg (2006)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-70545-1_8","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2008","unstructured":"Farzan, A., Madhusudan, P.: Monitoring Atomicity in Concurrent Programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 52\u201365. Springer, Heidelberg (2008)"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-02658-4_21","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2009","unstructured":"Farzan, A., Madhusudan, P.: Meta-analysis for Atomicity Violations under Nested Locking. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 248\u2013262. Springer, Heidelberg (2009)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-00768-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Farzan","year":"2009","unstructured":"Farzan, A., Madhusudan, P.: The Complexity of Predicting Atomicity Violations. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 155\u2013169. Springer, Heidelberg (2009)"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic Partial-Order Reduction for Model Checking Software. In: POPL 2005, pp. 110\u2013121 (2005)","DOI":"10.1145\/1047659.1040315"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Gupta, A.: Accelerating High-Level Bounded Model Checking. In: ICCAD 2006, pp. 794\u2013801 (2006)","DOI":"10.1109\/ICCAD.2006.320122"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/10722468_15","volume-title":"SPIN Model Checking and Software Verification","author":"K. Havelund","year":"2000","unstructured":"Havelund, K.: Using Runtime Analysis to Guide Model Checking of Java Programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 245\u2013264. Springer, Heidelberg (2000)"},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M.P. Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst.\u00a012, 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"11_CR12","unstructured":"http:\/\/incubator.apache.org\/thrift\/"},{"key":"11_CR13","unstructured":"Joint CAV\/ISSTA special event on specification, verification, and testing of concurrent software, \n                    \n                      http:\/\/research.microsoft.com\/qadeer\/cav_issta.html"},{"key":"11_CR14","unstructured":"http:\/\/www.princeton.edu\/~sinha\/CAV12_Traces.zip"},{"key":"11_CR15","unstructured":"Yices: An SMT solver, \n                    \n                      http:\/\/yices.csl.sri.com"},{"key":"11_CR16","unstructured":"Java grande forum benchmark suite, \n                    \n                      http:\/\/www2.epcc.ed.ac.uk\/computing\/research_activities\/java_grande\/index_1.html"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-642-14295-6_39","volume-title":"Computer Aided Verification","author":"V. Kahlon","year":"2010","unstructured":"Kahlon, V., Wang, C.: Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 434\u2013449. Springer, Heidelberg (2010)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM\u00a021(7) (1978)","DOI":"10.1145\/359545.359563"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering An Efficient SAT Solver. In: DAC 2001, New York, NY, USA, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"11_CR20","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and Reproducing Heisenbugs in Concurrent Programs. In: OSDI 2008, pp. 267\u2013280 (2008)"},{"key":"11_CR21","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an Abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland Procedure to DPLL(T). J. ACM\u00a053, 937\u2013977 (2006)","journal-title":"J. ACM"},{"issue":"4","key":"11_CR22","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1145\/322154.322158","volume":"26","author":"C.H. Papadimitriou","year":"1979","unstructured":"Papadimitriou, C.H.: The Serializability of Concurrent Database Updates. J. ACM\u00a026(4), 631\u2013653 (1979)","journal-title":"J. ACM"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"von Praun, C., Gross, T.R.: Static Detection of Atomicity Violations in Object-Oriented Programs. Object Technology\u00a03(6) (2004)","DOI":"10.5381\/jot.2004.3.6.a5"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Said, M., Wang, C., Sakalla, K., Yang, Z.: Generating Data Race Witnesses by an SMT-Based Analysis. In: NFMS (2011)","DOI":"10.1007\/978-3-642-20398-5_23"},{"issue":"4","key":"11_CR25","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.: Eraser: A Dynamic Data Race Detector for Multithreaded Programs. ACM Trans. Comput. Syst.\u00a015(4), 391\u2013411 (1997)","journal-title":"ACM Trans. Comput. Syst."},{"key":"11_CR26","unstructured":"Serb\u0103nut\u0103, T.F., Chen, F., Rosu, G.: Maximal Causal Models for Multithreaded Systems. Tech. Rep. UIUCDCS-R-2008-3017, UIUC"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Sinha, A., Malik, S.: Runtime Checking of Serializability in Software Transactional Memory. In: IPDPS, pp. 1\u201312 (2010)","DOI":"10.1109\/IPDPS.2010.5470389"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Sinha, A., Malik, S., Wang, C., Gupta, A.: Predictive Analysis for Detecting Serializability Errors through Trace Segmentation. In: MEMOCODE (2011)","DOI":"10.1109\/MEMCOD.2011.5970516"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Sinha, N., Wang, C.: Staged Concurrent Program Analysis. In: Foundations of Software Engineering, FSE (2010)","DOI":"10.1145\/1882291.1882301"},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"Sinha, N., Wang, C.: On interference abstractions. In: POPL 2011, pp. 423\u2013434 (2011)","DOI":"10.1145\/1925844.1926433"},{"key":"11_CR31","unstructured":"http:\/\/research.microsoft.com\/enus\/um\/redmond\/projects\/z3\/"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Wang, C., Chaudhuri, S., Gupta, A., Yang, Y.: Symbolic Pruning of Concurrent Program Executions. In: Foundations of Software Engineering (FSE), pp. 23\u201332 (2009)","DOI":"10.1145\/1595696.1595702"},{"key":"11_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-12002-2_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Wang","year":"2010","unstructured":"Wang, C., Limaye, R., Ganai, M., Gupta, A.: Trace-Based Symbolic Analysis for Atomicity Violations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 328\u2013342. Springer, Heidelberg (2010)"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-642-05089-3_17","volume-title":"FM 2009: Formal Methods","author":"C. Wang","year":"2009","unstructured":"Wang, C., Kundu, S., Ganai, M.K., Gupta, A.: Symbolic Predictive Analysis for Concurrent Programs. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 256\u2013272. Springer, Heidelberg (2009)"},{"key":"11_CR35","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.\u00a04963, pp. 382\u2013396. Springer, Heidelberg (2008)"},{"key":"11_CR36","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: A Runtime Model Checker for Multithreaded C Programs. Tech. Rep. UUCS-08-004, University of Utah (2008)"},{"key":"11_CR37","doi-asserted-by":"crossref","unstructured":"Yi, J., Sadowski, C., Flanagan, C.: SideTrack: Generalizing Dynamic Atomicity Analysis. In: PADTAD, pp. 1\u201310 (2009)","DOI":"10.1145\/1639622.1639630"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34188-5_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:08:02Z","timestamp":1558314482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34188-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642341878","9783642341885"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34188-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}