{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,6]],"date-time":"2026-11-06T18:08:32Z","timestamp":1793988512390,"version":"4.8.0"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2000,12,1]],"date-time":"2000-12-01T00:00:00Z","timestamp":975628800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,12,1]],"date-time":"2000-12-01T00:00:00Z","timestamp":975628800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order and Symbolic Computation"],"published-print":{"date-parts":[[2000,12]]},"DOI":"10.1023\/a:1026599015809","type":"journal-article","created":{"date-parts":[[2003,11,6]],"date-time":"2003-11-06T17:11:16Z","timestamp":1068138676000},"page":"315-353","source":"Crossref","is-referenced-by-count":86,"title":["Slicing Software for Model Construction"],"prefix":"10.1007","volume":"13","author":[{"given":"John","family":"Hatcliff","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hongjun","family":"Zheng","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"278952_CR1","unstructured":"Ball, T. and Horwitz, S. Slicing programs with arbitrary control-flow. In Lecture Notes in Computer Science, Vol. 749, Proceedings of the First International Workshop on Automated and Algorithmic Debugging, P. Fritzson (Ed.). Springer-Verlag, 1993."},{"key":"278952_CR2","unstructured":"Ball, T. and Horwitz, S. Slicing programs with arbitrary control flow (extended version). Technical Report 1128, University of Wisconsin, December 1992."},{"key":"278952_CR3","doi-asserted-by":"crossref","unstructured":"Bates, S. and Horwitz, S. Incremental program testing using program dependence graphs. In Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, January 1993, pp. 384\u2013396.","DOI":"10.1145\/158511.158694"},{"key":"278952_CR4","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., and Hwang, L.J. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, 1990, pp. 428\u2013439.","DOI":"10.1109\/LICS.1990.113767"},{"key":"278952_CR5","unstructured":"Cattel, T. Process control design using SPIN. In Proceedings of the First SPIN Workshop, October 1995."},{"key":"278952_CR6","unstructured":"Chang, J. and Richardson, D.J.H. Static and dynamic specification slicing. In Proceedings of the Fourth Irvine Software Symposium, April 1994."},{"issue":"4","key":"278952_CR7","doi-asserted-by":"crossref","first-page":"1097","DOI":"10.1145\/183432.183438","volume":"16","author":"J.D. Choi","year":"1994","unstructured":"Choi, J.D. and Ferrante, J. Static slicing in the presence of GOTO statements. ACMTransactions on Programming Languages and Systems, 16(4) (1994) 1097\u20131113.","journal-title":"ACMTransactions on Programming Languages and Systems"},{"key":"278952_CR8","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Giunchiglia, F., Mongardi, G., Torielli, F., and Traverso, P. Model checking safety critical software with SPIN: An application to a railway interlocking system. In Proceedings of the Third SPIN Workshop, April 1997.","DOI":"10.1007\/3-540-49646-7_22"},{"key":"278952_CR9","doi-asserted-by":"crossref","unstructured":"Cimitile, A., De Lucia, A., and Munro, M. Identifying reusable functions using specification driven program slicing: A case study. In Proceedings of the International Conference on Software Maintenance, G. Caldiera and K. Bennett (Eds.). Washington, October 1995, IEEE Computer Society Press, pp. 124\u2013133.","DOI":"10.1109\/ICSM.1995.526534"},{"key":"278952_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Fujita, M., Rajan, S.P., Reps, T., Shankar, S., and Teitelbaum, T. Program slicing of hardware description languages. In Proceedings of CHARME'99, September 1999.","DOI":"10.21236\/ADA363556"},{"issue":"5","key":"278952_CR11","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., and Long, D.E. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5) (1994) 1512\u20131542.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"278952_CR12","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Robby, and Hongjun 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"},{"issue":"3","key":"278952_CR13","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1109\/32.489078","volume":"22","author":"J.C. Corbett","year":"1996","unstructured":"Corbett, J.C. Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering, 22(3) (1996) 161\u2013180.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"278952_CR14","doi-asserted-by":"crossref","unstructured":"Cousot, P. and Cousot, R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, 1977, pp. 238\u2013252.","DOI":"10.1145\/512950.512973"},{"key":"278952_CR15","unstructured":"Dams, D. Abstract interpretation and partition refinement for model checking. PhD Thesis, Eindhoven University of Technology, July 1996."},{"issue":"2","key":"278952_CR16","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"Dams, D., Gerth, R., and Grumberg, O. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2) (1997) 253\u2013291.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"278952_CR17","unstructured":"Dwyer, M. and Hatcliff, J. Slicing software for model construction. In Proceedings of the 1999 ACMWorkshop on Partial Evaluation and Program Manipulation (PEPM'99), January 1999, O. Danvy (Ed.). BRICS Notes Series NS-99-1."},{"key":"278952_CR18","doi-asserted-by":"crossref","unstructured":"Dwyer, M., Hatcliff, J., and Nanda, M. Using partial evaluation to enable verification of concurrent software. ACM Computing Surveys, 30(es), September 1998. Special issue dedicated to 1998 Symposium on Partial Evaluation.","DOI":"10.1145\/289121.289143"},{"key":"278952_CR19","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B. and Pasareanu, C.S. Filter-based model checking of partial systems. In Proceedings of the Sixth ACM SIGSOFT Symposium on Foundations of Software Engineering, November 1998.","DOI":"10.1145\/288195.288307"},{"key":"278952_CR20","unstructured":"Dwyer, M.B. and Pasareanu, C.S. Model checking generic container implementations.Technical Report 98-10, Kansas State University, Department of Computing and Information Sciences, 1998."},{"key":"278952_CR21","unstructured":"Dwyer, M.B., Pasareanu, C.S., and Corbett, J.C. Translating Ada programs for model checking: A tutorial. Technical Report 98-12, Kansas State University, Department of Computing and Information Sciences, 1998."},{"key":"278952_CR22","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., and Corbett, J.C. Patterns in property specifications for finite-state verification. In Proceedings of the 21st International Conference on Software Engineering, May 1999.","DOI":"10.1145\/302405.302672"},{"key":"278952_CR23","unstructured":"Gamma, E., Helm, R., Johnson, R., and Vlissides, J. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1994."},{"key":"278952_CR24","doi-asserted-by":"crossref","unstructured":"Godefroid, P. and Wolper, P. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Proceedings of the Second Workshop on Computer Aided Verification, July 1991, pp. 417\u2013428.","DOI":"10.1007\/3-540-55179-4_32"},{"key":"278952_CR25","first-page":"1139","volume-title":"Information Processing '89. Proceedings of the IFIP 11th World Computer Congress","author":"C.K. Gomard","year":"1989","unstructured":"Gomard, C.K. and Jones, N.D. Compiler generation by partial evaluation. In Information Processing '89. Proceedings of the IFIP 11th World Computer Congress, G.X. Ritter (Ed.). IFIP, North-Holland, 1989, pp. 1139\u20131144."},{"key":"278952_CR26","doi-asserted-by":"crossref","unstructured":"Hatcliff, J. An introduction to partial evaluation using a simple flowchart language. In Proceedings of the 1998 DIKU International Summer School on Partial Evaluation, J. Hatcliff, P. Thiemann, and T. Mogensen (Eds.). number (to appear) in Tutorials in Computer Science, Copenhagen, Denmark, June 1998.","DOI":"10.1007\/3-540-47018-2_2"},{"key":"278952_CR27","first-page":"1","volume":"1694","author":"J. Hatcliff","year":"1999","unstructured":"Hatcliff, J., Corbett, J.C., Dwyer, M.B., Sokolowski, S., and Hongjun Zheng. A formal study of slicing for multi-threaded programs with JVM concurrency primitives. In Proceedings of the 6th International Static Analysis Symposium (SAS'99), September 1999. Lecture Notes in Computer Science, Vol. 1694 pp. 1\u201318.","journal-title":"Proceedings of the 6th International Static Analysis Symposium (SAS'99)"},{"key":"278952_CR28","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Dwyer, M.B., and Laubach, S. Staging static analysis using abstraction-based program specialization. In Principles of Declarative Programming 10th International Symposium, PLILP'98, September 1998. LNCS Vol. 1490.","DOI":"10.1007\/BFb0056612"},{"key":"278952_CR29","unstructured":"Hatcliff, J., Dwyer, M.B., Laubach, S., and Muhammad, N. Specializing configurable systems for finite-state verification. Technical Report 98\u20134, Kansas State University, Department of Computing and Information Sciences, 1998."},{"key":"278952_CR30","unstructured":"Hatcliff, J., Dwyer, M.B., and Hongjun Zheng. Slicing software for model construction (extended version). Technical Report 99\u201314, Kansas State University, Department of Computing and Information Sciences, 1999."},{"key":"278952_CR31","doi-asserted-by":"crossref","unstructured":"Heimdahl, M.P.E. and Whalen, M.W. Reduction and slicing of hierarchical state machines. In Lecture Notes in Computer Science, Vol. 1013, Proceedings of the Sixth European Software Engineering Conference (ESEC\/FSE 97), M. Jazayeri and H. Schauer (Eds.). Springer-Verlag, September 1997, pp. 450\u2013467.","DOI":"10.1007\/3-540-63531-9_30"},{"issue":"5","key":"278952_CR32","doi-asserted-by":"crossref","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, 23(5) (1997) 279\u2013294.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"278952_CR33","doi-asserted-by":"crossref","unstructured":"Horwitz, S., Prins, J., and Reps, T. On the adequacy of program dependence graphs for representing programs. In Proceedings of the Fifteenth Annual ACMSymposium on Principles of Programming Languages, San Diego, California, January 1988, pp. 146\u2013157.","DOI":"10.1145\/73560.73573"},{"key":"278952_CR34","unstructured":"Huth, M. and Ryan, M. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2000."},{"key":"278952_CR35","unstructured":"Millett, L.I. and Teitelbaum, T. Slicing Promela and its applications to model checking, simulation, and protocol understanding. In Proceedings of the 4th International SPIN Workshop, 1998."},{"key":"278952_CR36","unstructured":"Jones, N.D., Gomard, C.K., and Sestoft, P. Partial Evaluation and Automatic Program Generation. Prentice-Hall International, 1993."},{"issue":"1","key":"278952_CR37","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajiani, A., and Bensalem, S. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6(1) (1995) 11\u201344.","journal-title":"Formal Methods in System Design"},{"key":"278952_CR38","doi-asserted-by":"crossref","unstructured":"Manna, Z. and Pnueli, A. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"278952_CR39","doi-asserted-by":"crossref","unstructured":"McMillan, K.L. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"9","key":"278952_CR40","doi-asserted-by":"crossref","first-page":"965","DOI":"10.1109\/32.58784","volume":"16","author":"A. Podgurski","year":"1990","unstructured":"Podgurski, A. and Clarke, L.Aformal model of program dependences and its implications for software testing, debugging, and maintenance. IEEE Transactions on Software Engineering, 16(9) (1990) 965-979.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"278952_CR41","series-title":"Technical Report","volume-title":"Semantics of program representation graphs","author":"G. Ramalingam","year":"1989","unstructured":"Ramalingam, G. and Reps, T. Semantics of program representation graphs. Technical Report #900, University of Wisconsin, Madison, December 1989."},{"key":"278952_CR42","first-page":"409","volume-title":"Lecture Notes in Computer Science, Vol. 1110, Partial Evaluation. Dagstuhl Castle, Germany, February 1996","author":"T. Reps","year":"1996","unstructured":"Reps, T. and Turnidge, T. Program specialization via program slicing. In Lecture Notes in Computer Science, Vol. 1110, Partial Evaluation. Dagstuhl Castle, Germany, February 1996, O. Danvy, R. Gl\u00fcck, and P. Thiemann (Eds.). Springer-Verlag, Berlin, 1996, pp. 409\u2013429."},{"key":"278952_CR43","series-title":"Technical Report","volume-title":"The semantics of program slicing","author":"T. Reps","year":"1988","unstructured":"Reps, T. and Yang, W. The semantics of program slicing. Technical Report #777, Computer Sciences Department, University of Wisconsin, Madison, WI, June 1988."},{"key":"278952_CR44","volume-title":"Lecture Notes in Computer Science","author":"T. Reps","year":"1989","unstructured":"Reps, T. and Yang, W. The semantics of program slicing and program integration. In Proceedings of the Colloquium on Current Issues in Programming Languages, Barcelona, Spain, March 13\u201317, 1989. Lecture Notes in Computer Science, Springer-Verlag, New York, NY, March 1989."},{"key":"278952_CR45","first-page":"351","volume-title":"Lecture Notes in Computer Science, Vol. 1503, Proceedings of the 5th International Static Analysis Symposium (SAS'98)","author":"D. Schmidt","year":"1998","unstructured":"Schmidt, D. and Steffen, B. Program analysis as model checking of abstract interpretations. In Lecture Notes in Computer Science, Vol. 1503, Proceedings of the 5th International Static Analysis Symposium (SAS'98), G. Levi (Ed.). Springer-Verlag, Berlin, 1998, pp. 351\u2013380."},{"key":"278952_CR46","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1145\/229000.226315","volume-title":"Proceedings of the 1996 International Symposium on Software Testing and analysis","author":"A.M. Sloane","year":"1996","unstructured":"Sloane, A.M. and Holdsworth, J. Beyond traditional program slicing. In Proceedings of the 1996 International Symposium on Software Testing and analysis, S.J. Zeil (Ed.). ACM Press, New York, January 1996, pp. 180\u2013186."},{"key":"278952_CR47","first-page":"121","volume":"3","author":"F. Tip","year":"1995","unstructured":"Tip, F. A survey of program slicing techniques. Journal of programming languages, 3 (1995) 121\u2013189.","journal-title":"Journal of programming languages"},{"key":"278952_CR48","unstructured":"Vallee-Rai, R. and Hendren, L. Jimple: Simplifying Java bytecode for analyses and transformations. Technical Report 1998-4, Sable Research Group, School of Computer Science, McGill University, July 1998."},{"issue":"4","key":"278952_CR49","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1109\/TSE.1984.5010248","volume":"10","author":"M. Weiser","year":"1984","unstructured":"Weiser, M. Program slicing. IEEE Transactions on Software Engineering, SE-10(4) (1984) 352\u2013357.","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1026599015809.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1026599015809\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1026599015809.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T13:47:02Z","timestamp":1751982422000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1026599015809"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,12]]},"references-count":49,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2000,12]]}},"alternative-id":["278952"],"URL":"https:\/\/doi.org\/10.1023\/a:1026599015809","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,12]]}}}