{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:10:45Z","timestamp":1774987845487,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642050886","type":"print"},{"value":"9783642050893","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_17","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T17:31:40Z","timestamp":1257269500000},"page":"256-272","source":"Crossref","is-referenced-by-count":74,"title":["Symbolic Predictive Analysis for Concurrent Programs"],"prefix":"10.1007","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sudipta","family":"Kundu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Malay","family":"Ganai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"17_CR1","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":"17_CR2","volume-title":"Parallel and Distributed Processing Symposium (IPDPS)","author":"C. Flanagan","year":"2004","unstructured":"Flanagan, C., Freund, S.N.: Atomizer: A dynamic atomicity checker for multithreaded programs. In: Parallel and Distributed Processing Symposium (IPDPS). IEEE, Los Alamitos (2004)"},{"issue":"2","key":"17_CR3","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1109\/TSE.2006.1599419","volume":"32","author":"L. Wang","year":"2006","unstructured":"Wang, L., Stoller, S.D.: Runtime analysis of atomicity for multithreaded programs. IEEE Trans. Software Eng.\u00a032(2), 93\u2013110 (2006)","journal-title":"IEEE Trans. Software Eng."},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/11494881_14","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"K. Sen","year":"2005","unstructured":"Sen, K., Rosu, G., Agha, G.: Detecting errors in multithreaded programs by generalized predictive analysis of executions. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol.\u00a03535, pp. 211\u2013226. Springer, Heidelberg (2005)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-540-73368-3_27","volume-title":"Computer Aided Verification","author":"F. Chen","year":"2007","unstructured":"Chen, F., Rosu, G.: Parametric and sliced causality. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 240\u2013253. Springer, Heidelberg (2007)"},{"key":"17_CR6","unstructured":"Serb\u0103nut\u0103, T.F., Chen, F., Rosu, G.: Maximal causal models for multithreaded systems. Technical Report UIUCDCS-R-2008-3017, University of Illinois at Urbana-Champaign (2008)"},{"issue":"7","key":"17_CR7","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L. Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM\u00a021(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"17_CR8","volume-title":"Foundations of Software Engineering","author":"C. Wang","year":"2009","unstructured":"Wang, C., Chaudhuri, S., Gupta, A., Yang, Y.: Symbolic pruning of concurrent program executions. In: Foundations of Software Engineering. ACM, New York (2009)"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"17_CR10","first-page":"171","volume-title":"Principles of Programming Languages","author":"S. Lahiri","year":"2008","unstructured":"Lahiri, S., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: Principles of Programming Languages, pp. 171\u2013182. ACM, New York (2008)"},{"key":"17_CR11","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)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Lee, J., Padua, D., Midkiff, S.: Basic compiler algorithms for parallel programs. In: Principles and Practice of Parallel Programming, pp. 1\u201312 (1999)","DOI":"10.1145\/329366.301105"},{"key":"17_CR13","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":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1007\/978-3-642-02658-4_31","volume-title":"CAV 2009","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.\u00a05643, pp. 398\u2013413. Springer, Heidelberg (2009)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-71410-1_2","volume-title":"Logic-Based Program Synthesis and Transformation","author":"M. Musuvathi","year":"2007","unstructured":"Musuvathi, M., Qadeer, S.: CHESS: Systematic stress testing of concurrent software. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol.\u00a04407, pp. 15\u201316. Springer, Heidelberg (2007)"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-540-70545-1_7","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2008","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 37\u201351. Springer, Heidelberg (2008)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","first-page":"286","volume-title":"Parallel and Distributed Processing and Applications","author":"E. Farchi","year":"2003","unstructured":"Farchi, E., Nir, Y., Ur, S.: Concurrent bug patterns and how to test them. In: Guo, M. (ed.) ISPA 2003. LNCS, vol.\u00a02745, p. 286. Springer, Heidelberg (2003)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Principles of programming languages, pp. 110\u2013121 (2005)","DOI":"10.1145\/1047659.1040315"},{"issue":"8","key":"17_CR20","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1109\/2.84874","volume":"24","author":"C.J. Fidge","year":"1991","unstructured":"Fidge, C.J.: Logical time in distributed computing systems. IEEE Computer\u00a024(8), 28\u201333 (1991)","journal-title":"IEEE Computer"},{"key":"17_CR21","first-page":"12","volume-title":"Programming Language Design and Implementation","author":"S. Burckhardt","year":"2007","unstructured":"Burckhardt, S., Alur, R., Martin, M.: CheckFence: checking consistency of concurrent data types on relaxed memory models. In: Programming Language Design and Implementation, pp. 12\u201321. ACM, New York (2007)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/11513988_9","volume-title":"Computer Aided Verification","author":"I. Rabinovitz","year":"2005","unstructured":"Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 82\u201397. Springer, Heidelberg (2005)"},{"issue":"2","key":"17_CR23","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10703-005-1489-x","volume":"26","author":"P. Godefroid","year":"2005","unstructured":"Godefroid, P.: Software model checking: The VeriSoft approach. Formal Methods in System Design\u00a026(2), 77\u2013101 (2005)","journal-title":"Formal Methods in System Design"},{"key":"17_CR24","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: A Runtime Model Checker for Multithreaded C Programs. Technical Report UUCS-08-004, University of Utah (2008)"}],"container-title":["Lecture Notes in Computer Science","FM 2009: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05089-3_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:30:44Z","timestamp":1558269044000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}