{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T06:39:16Z","timestamp":1790836756610,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540851134","type":"print"},{"value":"9783540851141","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-85114-1_20","type":"book-chapter","created":{"date-parts":[[2008,8,13]],"date-time":"2008-08-13T03:22:48Z","timestamp":1218597768000},"page":"288-305","source":"Crossref","is-referenced-by-count":47,"title":["Efficient Stateful Dynamic Partial Order Reduction"],"prefix":"10.1007","author":[{"given":"Yu","family":"Yang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xiaofang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robert M.","family":"Kirby","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"20_CR1","first-page":"33","volume-title":"The problem with threads","author":"E.A. Lee","year":"2006","unstructured":"Lee, E.A.: The problem with threads, vol.\u00a039, pp. 33\u201342. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model Checking for Programming Languages using Verisoft. In: POPL, pp. 174\u2013186 (1997)","DOI":"10.1145\/263699.263717"},{"key":"20_CR3","first-page":"446","volume-title":"PLDI","author":"M. Musuvathi","year":"2007","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Ferrante, J., McKinley, K.S. (eds.) PLDI, pp. 446\u2013455. ACM, New York (2007)"},{"key":"20_CR4","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1145\/1040305.1040315","volume-title":"Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic Partial-order Reduction for Model Checking Software. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 110\u2013121. ACM, New York (2005)"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: A Pragmatic Approach to Model Checking Real Code. In: OSDI (2002)","DOI":"10.1145\/1060289.1060297"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S.: Model checking programs. In: ASE, pp. 3\u201312 (2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"20_CR7","unstructured":"http:\/\/www.cs.utah.edu\/~yuyang\/inspect"},{"key":"20_CR8","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1145\/1133981.1134019","volume-title":"PLDI","author":"P. Pratikakis","year":"2006","unstructured":"Pratikakis, P., Foster, J.S., Hicks, M.: Locksmith: context-sensitive correlation analysis for race detection. In: PLDI, pp. 320\u2013331. ACM Press, New York (2006)"},{"key":"20_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, Heidelberg (1996)"},{"key":"20_CR10","unstructured":"Palmer, R.L.: Formal Analysis for MPI-based High Performance Computing Software, Ph.D. Dissertation, University of Utah (2007)"},{"key":"20_CR11","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G.: UUCS-08-004:Inspect: A Runtime Model Checker for Multithreaded C Programs. Technical report (2008)"},{"key":"20_CR12","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/379539.379553","volume-title":"PPoPP","author":"A. Salcianu","year":"2001","unstructured":"Salcianu, A., Rinard, M.: Pointer and escape analysis for multithreaded programs. In: PPoPP, pp. 12\u201323. ACM Press, New York (2001)"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-73370-6_8","volume-title":"Model Checking Software","author":"G. Gueta","year":"2007","unstructured":"Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Bosnacki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 95\u2013112. Springer, Heidelberg (2007)"},{"key":"20_CR14","unstructured":"http:\/\/bzip2smp.sourceforge.net\/"},{"key":"20_CR15","unstructured":"http:\/\/freshmeat.net\/projects\/pfscan"},{"key":"20_CR16","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: Bogor: an extensible and highly-modular software model checking framework. In: ESEC \/ SIGSOFT FSE, pp. 267\u2013276 (2003)","DOI":"10.1145\/949952.940107"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/11901433_9","volume-title":"Formal Methods and Software Engineering","author":"X. Yi","year":"2006","unstructured":"Yi, X., Wang, J., Yang, X.: Stateful Dynamic Partial-Order Reduction. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 149\u2013167. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-85114-1_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,19]],"date-time":"2023-05-19T15:15:55Z","timestamp":1684509355000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85114-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540851134","9783540851141"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85114-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}