{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:34:54Z","timestamp":1791459294446,"version":"4.3.4"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642203978","type":"print"},{"value":"9783642203985","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-20398-5_23","type":"book-chapter","created":{"date-parts":[[2011,4,6]],"date-time":"2011-04-06T19:29:49Z","timestamp":1302118189000},"page":"313-327","source":"Crossref","is-referenced-by-count":50,"title":["Generating Data Race Witnesses by an SMT-Based Analysis"],"prefix":"10.1007","author":[{"given":"Mahmoud","family":"Said","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zijiang","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Karem","family":"Sakallah","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"23_CR1","first-page":"56","volume-title":"OOPSLA 2001. SIGPLAN Notices","author":"C. Boyapati","year":"2001","unstructured":"Boyapati, C., Rinard, M.C.: A parameterized type system for race-free Java programs. In: OOPSLA 2001. SIGPLAN Notices, vol.\u00a036(11), pp. 56\u201369. ACM, New York (2001)"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Wang, C., Mahmoud\u00a0Said, A.G.: Coverage guided systematic concurrency testing. In: International Conference on Software Engineering, ICSE 2011 (2011)","DOI":"10.1145\/1985793.1985824"},{"key":"23_CR3","unstructured":"Christey, S. (ed.): Top 25 most dangerous programming errors. CWE\/SANS report (2009), http:\/\/cwe.mitre.org\/top25\/"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"issue":"6","key":"23_CR5","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/1273442.1250762","volume":"42","author":"T. Elmas","year":"2007","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: a race and transaction-aware Java runtime. j-SIGPLAN\u00a042(6), 245\u2013255 (2007)","journal-title":"j-SIGPLAN"},{"key":"23_CR6","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1145\/945445.945468","volume-title":"ACM Symposium on Operating Systems Principles","author":"D. Engler","year":"2003","unstructured":"Engler, D., Ashcraft, K.: RacerX: effective, static detection of race conditions and deadlocks. In: ACM Symposium on Operating Systems Principles, pp. 237\u2013252. ACM, New York (2003)"},{"key":"23_CR7","first-page":"286","volume-title":"Parallel and Distributed Processing","author":"E. Farchi","year":"2003","unstructured":"Farchi, E., Nir, Y., Ur, S.: Concurrent bug patterns and how to test them. In: Parallel and Distributed Processing, p. 286.2. IEEE Computer Society, Washington, DC (2003)"},{"key":"23_CR8","first-page":"219","volume-title":"Programming Language Design and Implementation","author":"C. Flanagan","year":"2000","unstructured":"Flanagan, C., Freund, S.: Type-based race detection for Java. In: Programming Language Design and Implementation, pp. 219\u2013232. ACM, New York (2000)"},{"key":"23_CR9","first-page":"121","volume-title":"Programming Language Design and Implementation","author":"C. Flanagan","year":"2009","unstructured":"Flanagan, C., Freund, S.N.: Fasttrack: efficient and precise dynamic race detection. In: Programming Language Design and Implementation, pp. 121\u2013133. ACM, New York (2009)"},{"key":"23_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)"},{"issue":"4","key":"23_CR11","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA PathFinder. International Journal on Software Tools for Technology Transfer (STTT)\u00a02(4), 366\u2013381 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"23_CR12","unstructured":"Joint cav\/issta special even on specification, verification, and testing of concurrent software, http:\/\/research.microsoft.com\/qadeer\/cavissta.htm"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-540-73368-3_26","volume-title":"Computer Aided Verification","author":"V. Kahlon","year":"2007","unstructured":"Kahlon, V., Yang, Y., Sankaranarayanan, S., Gupta, A.: Fast and accurate static data-race detection for concurrent programs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 226\u2013239. Springer, Heidelberg (2007)"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/11513988_49","volume-title":"Computer Aided Verification","author":"V. Kahlon","year":"2005","unstructured":"Kahlon, V., Ivancic, F., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 505\u2013518. Springer, Heidelberg (2005)"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The java memory model. In: Principles of Programming Languages (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"23_CR16","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Musuvathi, M., Qadeer, S., Ball, T.: Chess: A systematic testing tool for concurrent software. Tech. Rep. MSR-TR-2007-149, Microsoft Research (2007)"},{"key":"23_CR17","volume-title":"Principles of programming languages","author":"M. Naik","year":"2007","unstructured":"Naik, M., Aiken, A.: Conditional must not aliasing for static race detection. In: Principles of programming languages. ACM, New York (2007)"},{"key":"23_CR18","first-page":"320","volume-title":"Programming Language Design and Implementation","author":"P. Pratikakis","year":"2006","unstructured":"Pratikakis, P., Foster, J., Hicks, M.: LOCKSMITH: context-sensitive correlation analysis for race detection. In: Programming Language Design and Implementation, pp. 320\u2013331. ACM, New York (2006)"},{"key":"23_CR19","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":"23_CR20","unstructured":"The java grande forum benchmark suite, http:\/\/www2.epcc.ed.ac.uk\/computing\/research_activities\/java_grande\/index_1.html"},{"issue":"4","key":"23_CR21","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.E.: Eraser: A dynamic data race detector for multi-threaded programs. ACM Trans. Comput. Syst.\u00a015(4), 391\u2013411 (1997)","journal-title":"ACM Trans. Comput. Syst."},{"key":"23_CR22","unstructured":"Serb\u0103nut\u0103, T.F., Chen, F., Rosu, G.: Maximal causal models for multithreaded systems. Tech. Rep. UIUCDCS-R-2008-3017, University of Illinois at Urbana-Champaign (2008)"},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using model checking with symbolic execution to verify parallel numerical programs. In: ISSTA (2006)","DOI":"10.1145\/1146238.1146256"},{"key":"23_CR24","first-page":"205","volume-title":"Foundations of Software Engineering","author":"J. Voung","year":"2007","unstructured":"Voung, J., Jhala, R., Lerner, S.: RELAY: static race detection on millions of lines of code. In: Foundations of Software Engineering, pp. 205\u2013214. ACM, New York (2007)"},{"key":"23_CR25","volume-title":"International Symposium on Formal Methods","author":"C. Wang","year":"2009","unstructured":"Wang, C., Kundu, S., Ganai, M., Gupta, A.: Symbolic predictive analysis for concurrent programs. In: International Symposium on Formal Methods. ACM, New York (2009)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-20398-5_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,21]],"date-time":"2021-11-21T06:48:23Z","timestamp":1637477303000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-20398-5_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642203978","9783642203985"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-20398-5_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}