{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:55Z","timestamp":1762458595524},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422877"},{"type":"electronic","value":"9783540482246"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-48224-5_54","type":"book-chapter","created":{"date-parts":[[2007,10,28]],"date-time":"2007-10-28T06:29:04Z","timestamp":1193552944000},"page":"652-666","source":"Crossref","is-referenced-by-count":27,"title":["Model Checking of Unrestricted Hierarchical State Machines"],"prefix":"10.1007","author":[{"given":"Michael","family":"Benedikt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrice","family":"Godefroid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"54_CR1","unstructured":"A. Aho, J. Hopcroft, and J. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, 1974."},{"key":"54_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, K. Etessami, and M. Yannakakis. Analysis of Recursive State Machines. In To appear in Proceedings of CAV 2001, Paris, July 2001.","DOI":"10.1007\/3-540-44585-4_18"},{"key":"54_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur and R. Grosu. Modular Refinement of Hierarchic State Machines. In Proceedings of the 27th ACM Symposium on Principles of Programming Languages, pages 390\u2013402, January 2000.","DOI":"10.1145\/325694.325746"},{"key":"54_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-48523-6_14","volume-title":"Proceedings of the 26th International Colloquium on Automata, Languages, and Programming","author":"R. Alur","year":"1999","unstructured":"R. Alur, S. Kannan, and M. Yannakakis. Communicating Hierarchical State Machines. In Proceedings of the 26th International Colloquium on Automata, Languages, and Programming, volume 1644 of Lecture Notes in Computer Science, pages 169\u2013178. Springer-Verlag, 1999."},{"key":"54_CR5","doi-asserted-by":"crossref","unstructured":"R. Alur and M. Yannakakis. Model Checking of Hierarchical State Machines. In Proceedings of the Sixth ACM Symposium on the Foundations of Software Engineering (FSE\u201998), pages 175\u2013188, 1998.","DOI":"10.1145\/288195.288305"},{"key":"54_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"Proc. of CONCUR\u201997","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability Analysis of Pushdown Automata: Application to Model-Checking. In Proc. of CONCUR\u201997, volume 1243 of Lecture Notes in Computer Science, pages 135\u2013150. Springer-Verlag, 1997."},{"key":"54_CR7","doi-asserted-by":"crossref","unstructured":"O. Burkart and B. Steffen. Model Checking for Context-Free Processes. In Proc. of CONCUR\u201992, 1992.","DOI":"10.1007\/BFb0084787"},{"key":"54_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/3-540-63165-8_198","volume-title":"Proc. of ICALP\u201997","author":"O. Burkart","year":"1997","unstructured":"O. Burkart and B. Steffen. Model Checking the Full Modal Mu-Calculus for Infinite Sequential Processes. In Proc. of ICALP\u201997, volume 1256 of Lecture Notes in Computer Science, pages 419\u2013429, Bologna, 1997. Springer-Verlag."},{"key":"54_CR9","series-title":"Lect Notes Comput Sci","first-page":"311","volume-title":"Graph Theoretic Concepts in Computer Science","author":"B. Caucal","year":"1990","unstructured":"B. Caucal and R. Monfort. On the Transition Graphs of Automata and Grammars. In Graph Theoretic Concepts in Computer Science, volume 484 of Lecture Notes in Computer Science, pages 311\u2013337. Springer-Verlag, 1990."},{"key":"54_CR10","volume-title":"Handbook of Theoretical Computer Science","author":"E. A. Emerson","year":"1990","unstructured":"E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. Elsevier\/MIT Press, Amsterdam\/Cambridge, 1990."},{"key":"54_CR11","unstructured":"E. A. Emerson and C. Lei. Efficient Model Checking in Fragments of the Propositional Mu-Calculus. In Proceedings of the First Symposium on Logic in Computer Science, pages 267\u2013278, Cambridge, June 1986."},{"key":"54_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Proceedings of the 12th Conference on Computer Aided Verification","author":"J. Esparza","year":"2000","unstructured":"J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient Algorithms for Model Checking Pushdown Systems. In Proceedings of the 12th Conference on Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 232\u2013247, Chicago, July 2000. Springer-Verlag."},{"key":"54_CR13","doi-asserted-by":"crossref","unstructured":"A. Finkel, B. Willems, and P. Wolper. A Direct Symbolic Approach to Model Checking Pushdown Systems. Electronic Notes in Theoretical Comp. Sc., 9, 1997.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"54_CR14","unstructured":"J. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979."},{"key":"54_CR15","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1145\/222124.222146","volume-title":"Proceedings of the Third ACM SIGSOFT Symposium on the Foundations of Software Engineering","author":"S. Horwitz","year":"1995","unstructured":"S. Horwitz, T. Reps, and M. Sagiv. Demand interprocedural dataflow analysis. In Proceedings of the Third ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 104\u2013115, New York, NY, October 1995. ACM Press."},{"key":"54_CR16","first-page":"11","volume-title":"Proceedings of the Third ACM SIGSOFT Symposium on the Foundations of Software Engineering","author":"S. Horwitz","year":"1994","unstructured":"S. Horwitz, T. Reps, M. Sagiv, and G. Rosay. Speeding up slicing. In Proceedings of the Third ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 11\u201320, New York, NY, December 1994. ACM Press."},{"issue":"11","key":"54_CR17","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1016\/S0950-5849(98)00093-7","volume":"40","author":"T. Reps","year":"1998","unstructured":"T. Reps. Program analysis via graph reachability. Information and Software Technology, 40(11-12):701\u2013726, November 1998. Special issue on program slicing.","journal-title":"Information and Software Technology"},{"key":"54_CR18","first-page":"49","volume-title":"Symp. on Princ. of Prog. Lang.","author":"T. Reps","year":"1995","unstructured":"T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Symp. on Princ. of Prog. Lang., pages 49\u201361, New York, NY, 1995. ACM Press."},{"key":"54_CR19","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322\u2013331, Cambridge, June 1986."},{"key":"54_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-61474-5_58","volume-title":"Proc. 8th Conference on Computer Aided Verification","author":"I. Walukiewicz","year":"1996","unstructured":"I. Walukiewicz. Pushdown Processes: Games and Model-Checking. In Proc. 8th Conference on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 62\u201374, New Brunswick, August 1996. Springer-Verlag."},{"key":"54_CR21","doi-asserted-by":"crossref","unstructured":"M. Yannakakis. Graph-theoretic methods in database theory. In Proc. of the Symp. on Princ. of Database Syst., pages 230\u2013242, 1990.","DOI":"10.1145\/298514.298576"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48224-5_54","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T02:28:13Z","timestamp":1556936893000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48224-5_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422877","9783540482246"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-48224-5_54","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}