{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:50:25Z","timestamp":1743141025291,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540883869"},{"type":"electronic","value":"9783540883876"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-88387-6_11","type":"book-chapter","created":{"date-parts":[[2008,10,10]],"date-time":"2008-10-10T05:42:45Z","timestamp":1223617365000},"page":"126-140","source":"Crossref","is-referenced-by-count":26,"title":["Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions"],"prefix":"10.1007","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[]},{"given":"Yu","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"International Conference on Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: International Conference on Concurrency Theory. LNCS, vol.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"11_CR2","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":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proceedings Workshop on Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proceedings Workshop on Logics of Programs. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1981)"},{"key":"11_CR4","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":"11_CR5","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"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K., Lillibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended static checking for java. In: PLDI, pp. 234\u2013245 (2002)","DOI":"10.1145\/543552.512558"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Ganai, M., Kundu, S., Gupta, R.: Partial order reduction for scalable testing of SystemC TLM designs. In: Design Automation Conference (2008)","DOI":"10.1145\/1391469.1391706"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)"},{"issue":"2","key":"11_CR9","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"},{"issue":"4","key":"11_CR10","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/s100090050039","volume":"2","author":"G. Holzmann","year":"2000","unstructured":"Holzmann, G., Najm, E., Serhrouchni, A.: SPIN model checking: An introduction. STTT\u00a02(4), 321\u2013327 (2000)","journal-title":"STTT"},{"key":"11_CR11","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)"},{"issue":"7","key":"11_CR12","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/MC.1993.274940","volume":"26","author":"N. Leveson","year":"1993","unstructured":"Leveson, N., Turner, C.: Investigation of the therac-25 accidents. IEEE Computer\u00a026(7), 18\u201341 (1993)","journal-title":"IEEE Computer"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","first-page":"279","volume-title":"Advances in Petri Nets 1986. Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986","author":"A.W. Mazurkiewicz","year":"1987","unstructured":"Mazurkiewicz, A.W.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol.\u00a0255, pp. 279\u2013324. Springer, Heidelberg (1987)"},{"key":"11_CR14","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":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G. Necula","year":"2002","unstructured":"Necula, G., McPeak, S., Rahul, S., Weimer, W.: Cil: Intermediate language and tools for analysis and transformation of c programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol.\u00a02304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Nethercote, N., Seward, J.: Valgrind: A program supervision framework. Electr. Notes Theor. Comput. Sci.\u00a089(2) (2003)","DOI":"10.1016\/S1571-0661(04)81042-9"},{"key":"11_CR17","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., Hicks, M.: LOCKSMITH: context-sensitive correlation analysis for race detection. In: PLDI, pp. 320\u2013331. ACM, New York (2006)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proceedings of the Fifth Annual Symposium on Programming (1981)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"11_CR19","first-page":"12","volume-title":"Principles and Practices of Parallel Programming","author":"A. Salcianu","year":"2001","unstructured":"Salcianu, A., Rinard, M.: Pointer and escape analysis for multithreaded programs. In: Principles and Practices of Parallel Programming, pp. 12\u201323. ACM Press, New York (2001)"},{"issue":"4","key":"11_CR20","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_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"11_CR22","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":"11_CR23","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)"},{"key":"11_CR24","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G., Kirby, R.: Efficient stateful dynamic partial order reduction. In: SPIN Workshop on Model Checking Software (2008)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88387-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,20]],"date-time":"2023-05-20T10:22:22Z","timestamp":1684578142000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88387-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540883869","9783540883876"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88387-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}