{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T09:52:43Z","timestamp":1790934763302,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540330561","type":"print"},{"value":"9783540330578","type":"electronic"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006]]},"DOI":"10.1007\/11691372_5","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T14:22:26Z","timestamp":1143555746000},"page":"73-89","source":"Crossref","is-referenced-by-count":35,"title":["Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs"],"prefix":"10.1007","author":[{"given":"Matthew B.","family":"Dwyer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew","family":"Hoosier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Venkatesh","family":"Ranganath","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"family":"Robby","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Todd","family":"Wallentine","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"5_CR1","volume-title":"Concurrent Programming: Principles and Practice","author":"G.R. Andrews","year":"1991","unstructured":"Andrews, G.R.: Concurrent Programming: Principles and Practice. Addison-Wesley, Reading (1991)"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation (PLDI 2001), June 2001, pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"key":"5_CR3","unstructured":"Bandera. SAnToS Laboratory, http:\/\/bandera.projects.cis.ksu.edu"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/10722167_41","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"2000","unstructured":"Bozga, M., Fernandez, J.-C., Ghirvu, L., Graf, S., Krimm, J.-P., Mounier, L.: IF: A validation environment for timed asynchronous systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 543\u2013547. Springer, Heidelberg (2000)"},{"key":"5_CR5","unstructured":"Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder \u2013 A second generation of a Java model-checker. In: Proceedings of the Workshop on Advances in Verification (July 2000)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-48153-2_22","volume-title":"Correct Hardware Design and Verification Methods","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Fujita, M., Rajan, S.P., Reps, T., Shankar, S., Teitelbaum, T.: Program slicing of hardware description languages. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 298\u2013313. Springer, Heidelberg (1999)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","first-page":"52","volume-title":"Logic 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: Engeler, E. (ed.) Logic of Programs 1979. LNCS, vol.\u00a0125, pp. 52\u201371. Springer, Heidelberg (1981)"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Robby, Zheng, H.: Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In: Proceedings of the 22nd International Conference on Software Engineering (June 2000)","DOI":"10.1145\/337180.337234"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby: Expressing checkable properties of dynamic systems: The Bandera Specification Language. International Journal on Software Tools for Technology Transfer (2002)","DOI":"10.1007\/s100090200075"},{"key":"5_CR10","first-page":"60","volume-title":"2004 International Symposium on Empirical Software Engineering (ISESE 2004)","author":"H. Do","year":"2004","unstructured":"Do, H., Elbaum, S., Rothermel, G.: Infrastructure support for controlled experimentation with software testing and regression testing techniques. In: 2004 International Symposium on Empirical Software Engineering (ISESE 2004), pp. 60\u201370. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"5_CR11","unstructured":"Dwyer, M.B., Hatcliff, J., Joehanes, R., Laubach, S., P\u02d8as\u02d8areanu, C.S., P\u0103s\u0103reanu, C.S., Robby, Visser, W., Zheng, H.: Tool-supported program abstraction for finite-state verification. In: Proceedings of the 23rd International Conference on Software Engineering (May 2001)"},{"issue":"2\u20133","key":"5_CR12","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/B:FORM.0000040028.49845.67","volume":"25","author":"M.B. Dwyer","year":"2004","unstructured":"Dwyer, M.B., Hatcliff, J., Prasad, V.R., Robby: Exploiting object escape and locking information in partial order reductions for concurrent object-oriented programs. Formal Methods in System Designs\u00a025(2\u20133), 199\u2013240 (2004)","journal-title":"Formal Methods in System Designs"},{"key":"5_CR13","unstructured":"Eclipse Consortium. Eclipse website, http:\/\/www.eclipse.org"},{"key":"5_CR14","first-page":"110","volume-title":"Proceedings of the 32nd ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL","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 ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, Long Beach, California, USA, January 2005, pp. 110\u2013121. ACM, New York (2005)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032. Springer, Heidelberg (1996)"},{"key":"5_CR16","first-page":"12","volume-title":"Proceedings of the International Symposium on Software Testing and Analysis","author":"A. Groce","year":"2002","unstructured":"Groce, A., Visser, W.: Model checking Java programs using structural heuristics. In: Proceedings of the International Symposium on Software Testing and Analysis, pp. 12\u201321. ACM Press, New York (2002)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-48294-6_1","volume-title":"Static Analysis","author":"J. Hatcliff","year":"1999","unstructured":"Hatcliff, J., Corbett, J., Dwyer, M.B., Sokolowski, S., Zheng, H.: A formal study of slicing for multi-threaded programs with JVM concurrency primitives. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol.\u00a01694, p. 1. Springer, Heidelberg (1999)"},{"issue":"4","key":"5_CR18","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1023\/A:1026599015809","volume":"13","author":"J. Hatcliff","year":"2000","unstructured":"Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. Journal of Higher-order and Symbolic Computation\u00a013(4), 315\u2013353 (2000)","journal-title":"Journal of Higher-order and Symbolic Computation"},{"issue":"5","key":"5_CR19","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013294 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5_CR20","unstructured":"Holzmann, G.J.: Personal communication (October 2005)"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-46017-9_5","volume-title":"Model Checking Software","author":"R. Iosif","year":"2002","unstructured":"Iosif, R.: Symmetry Reduction Criteria for Software Model Checking. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 22\u201341. Springer, Heidelberg (2002)"},{"key":"5_CR22","unstructured":"Java Grande Benchmarking Project. Java Grande forum benchmark suite \u2013 thread version 1.0., http:\/\/www.epcc.ed.ac.uk\/computing\/researchactivities\/javagrande\/"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-540-31984-9_20","volume-title":"Fundamental Approaches to Software Engineering","author":"G. Jayaraman","year":"2005","unstructured":"Jayaraman, G., Ranganath, V.P., Hatcliff, J.: Kaveri: Delivering the Indus Java Program Slicer to Eclipse. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol.\u00a03442, pp. 269\u2013272. Springer, Heidelberg (2005)"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/3-540-45139-0_8","volume-title":"Model Checking Software","author":"G. Jia","year":"2001","unstructured":"Jia, G., Graf, S.: Verification experiments on the MASCARA protocol. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 123\u2013142. Springer, Heidelberg (2001)"},{"key":"5_CR25","series-title":"ACM SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1145\/277631.277638","volume-title":"Proceedings ACM SIGPLAN\/SIGFSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 1998)","author":"J. Krinke","year":"1998","unstructured":"Krinke, J.: Static slicing of threaded programs. In: Proceedings ACM SIGPLAN\/SIGFSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 1998), June 1998. ACM SIGPLAN Notices, vol.\u00a033(7), pp. 35\u201342. ACM Press, New York (1998)"},{"key":"5_CR26","unstructured":"Millett, L.I., Teitelbaum, T.: Slicing Promela and its applications to model checking, simulation, and protocol understanding. In: Proceedings of the 4th International SPIN Workshop. LNCS (1998)"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Nanda, M.G., Ramesh, S.: Slicing concurrent programs. In: Proceedings of International Symposium on Software Testing and Analysis (ISSTA 2000), pp. 180\u2013190 (2000)","DOI":"10.1145\/347324.349121"},{"issue":"8","key":"5_CR28","doi-asserted-by":"publisher","first-page":"965","DOI":"10.1109\/32.58784","volume":"16","author":"A. Podgurski","year":"1990","unstructured":"Podgurski, A., Clarke, L.: A formal model of program dependences and its implications for software testing, debugging, and maintenance. IEEE Transactions on Software Engineering\u00a016(8), 965\u2013979 (1990)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5_CR29","unstructured":"Ranganath, V.P.: Indus, http:\/\/indus.projects.cis.ksu.edu"},{"key":"5_CR30","unstructured":"Ranganath, V.P.: Object-flow analysis for optimizing finite-state models of Java software. Master\u2019s thesis, Kansas State University (2002)"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-31987-0_7","volume-title":"Programming Languages and Systems","author":"V.P. Ranganath","year":"2005","unstructured":"Ranganath, V.P., Amtoft, T., Banerjee, A., Dwyer, M.B., Hatcliff, J.: A new foundation for control-dependence and slicing for modern program structures. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 77\u201393. Springer, Heidelberg (2005)"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-540-24723-4_4","volume-title":"Compiler Construction","author":"V.P. Ranganath","year":"2004","unstructured":"Ranganath, V.P., Hatcliff, J.: Pruning interference and ready dependences for slicing concurrent Java programs. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol.\u00a02985, pp. 39\u201356. Springer, Heidelberg (2004)"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M.B., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 9th European Software Engineering Conference \/ 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering (2003)","DOI":"10.1145\/940103.940107"},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M.B., Hatcliff, J., Iosif, R.: Space-reduction strategies for model checking dynamic systems. In: Proceedings of the 2003 Workshop on Software Model Checking (July 2003)","DOI":"10.1007\/978-3-540-45212-6_12"},{"key":"5_CR35","doi-asserted-by":"crossref","unstructured":"Sen, A., Bhadra, J., Garg, V.K., Abraham, J.A.: Formal verification of a system-on-chip using computation slicing. In: International Test Conference ITC, October 2004, pp. 810\u2013819 (2004)","DOI":"10.1109\/TEST.2004.1387344"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Stoller, S.: Model-checking multi-threaded distributed Java programs. International Journal on Software Tools for Technology Transfer (2002)","DOI":"10.1007\/s10009-002-0077-2"},{"key":"5_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/978-3-540-31980-1_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Suwimonteerabuth","year":"2005","unstructured":"Suwimonteerabuth, D., Schwoon, S., Esparza, J.: jMoped: A Java bytecode checker based on Moped. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 541\u2013545. Springer, Heidelberg (2005)"},{"key":"5_CR38","first-page":"121","volume":"3","author":"F. Tip","year":"1995","unstructured":"Tip, F.: A survey of program slicing techniques. Journal of programming languages\u00a03, 121\u2013189 (1995)","journal-title":"Journal of programming languages"},{"key":"5_CR39","unstructured":"Vall\u00e9e-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., Co, P.: Soot \u2013 A Java optimization framework. In: Proceedings of CASCON 1999 (November 1999)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11691372_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,17]],"date-time":"2019-04-17T17:19:48Z","timestamp":1555521588000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11691372_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540330561","9783540330578"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/11691372_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}