{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:40:42Z","timestamp":1725493242609},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651918"},{"type":"electronic","value":"9783540495192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49519-3_30","type":"book-chapter","created":{"date-parts":[[2007,10,20]],"date-time":"2007-10-20T06:37:12Z","timestamp":1192862232000},"page":"469-481","source":"Crossref","is-referenced-by-count":4,"title":["Techniques for Implicit State Enumeration of EFSMs"],"prefix":"10.1007","author":[{"given":"James H.","family":"Kukula","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas R.","family":"Shiple","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adnan","family":"Aziz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"30_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-60045-0_38","volume-title":"Proc. Computer Aided Verification","author":"D. A. Basin","year":"1995","unstructured":"D. A. Basin and N. Klarlund. Hardware verification using monadic second-order logic. In P. Wolper, editor, Proc. Computer Aided Verification, volume 939 of LNCS, pages 31\u201341. Springer-Verlag, July 1995."},{"key":"30_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/3-540-61064-2_27","volume-title":"Trees and Algebra in Programming-CAAP","author":"A. Boudet","year":"1996","unstructured":"A. Boudet and H. Comon. Diophantine equations, Presburger arithmetic and finite automata. In H. Kirchner, editor, Trees and Algebra in Programming-CAAP, volume 1059 of LNCS, pages 30\u201343. Springer-Verlag, 1996."},{"key":"30_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Proceedings of the Conference on Computer-Aided Verification","author":"R. K. Brayton","year":"1996","unstructured":"R. K. Brayton, G. D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy, and T. Villa. VIS: A system for verification and synthesis. In R. Alur and T. A. Henzinger, editors, Proceedings of the Conference on Computer-Aided Verification, volume 1102 of LNCS, pages 428\u2013432, New Brunswick NJ, July 1996. Springer-Verlag."},{"key":"30_CR4","unstructured":"J. R. B\u00fcchi. On a decision method in restricted second order arithmetic. In Proc. Int. Congress Logic, Methodology, and Philosophy of Science, pages 1\u201311, Berkeley CA, 1960. Stanford University Press."},{"key":"30_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Proc. Computer Aided Verification","author":"T. Bultan","year":"1997","unstructured":"T. Bultan, R. Geber, and W. Pugh. Symbolic model checking of infinite state programs using Presburger arithmetic. In O. Grumberg, editor, Proc. Computer Aided Verification, volume 1254 of LNCS, pages 400\u2013411, Haifa, June 1997. Springer-Verlag."},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"K.-T. Cheng and A. Krishnakumar. Automatic functional test generation using the extended finite state machine model. In Proc. 30th Design Automat. Conf., pages 86\u201391, June 1993.","DOI":"10.1145\/157485.164585"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. in Proc. Principles of Programming Language, Jan. 1992","DOI":"10.1145\/143165.143235"},{"key":"30_CR8","series-title":"Lect Notes Comput Sci","first-page":"365","volume-title":"Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems","author":"O. Coudert","year":"1989","unstructured":"O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In J. Sifakis, editor, Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pages 365\u2013373. Springer-Verlag, June 1989."},{"key":"30_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/3-540-58179-0_59","volume-title":"Proc. Computer Aided Verification","author":"D. Cyrluk","year":"1994","unstructured":"D. Cyrluk and P. Narendran. Ground temporal logic: A logic for hardware verification. In D. L. Dill, editor, Proc. Computer Aided Verification, volume 818 of LNCS, pages 247\u2013259, Stanford, CA, June 1994. Springer-Verlag."},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"P. Godefroid and D. E. Long. Symbolic protocol verification with queue BDDs. In Proc. Logic in Computer Science, pages 198\u2013206, July 1996.","DOI":"10.1109\/LICS.1996.561318"},{"key":"30_CR11","unstructured":"A. Gupta. Inductive Boolean Function Manipulation: A Hardware Verification Methodology for Automatic Induction. PhD thesis, Carnegie Mellon University, 1994. Memorandum No. CMU-CS-94-208."},{"key":"30_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS\u2019 95","author":"J. G. Henriksen","year":"1995","unstructured":"J. G. Henriksen, J. Jensen, M. J\u00d8rgensen, N. Klarlund, R. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS\u2019 95, volume 1019 of LNCS, pages 89\u2013110. Springer-Verlag, May 1995."},{"key":"30_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/3-540-60045-0_43","volume-title":"Proc. Computer Aided Verification","author":"R. Hojati","year":"1995","unstructured":"R. Hojati and R. K. Brayton. Automatic datapath abstraction in hardware systems. In P. Wolper, editor, Proc. Computer Aided Verification, volume 939 of LNCS, pages 98\u2013113. Springer-Verlag, July 1995."},{"key":"30_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BFb0035388","volume-title":"TACAS\u2019 97: Int\u2019l Workshop on Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Kelb","year":"1997","unstructured":"P. Kelb, T. Margaria, M. Mendler, and C. Gsottberger. MOSEL: A flexible toolset for monadic second-order logic. In TACAS\u2019 97: Int\u2019l Workshop on Tools and Algorithms for the Construction and Analysis of Systems, volume 1217 of LNCS, pages 183\u2013202. Springer-Verlag, Apr. 1997."},{"key":"30_CR15","unstructured":"W. Kelly, V. Maslov, W. Pugh, E. Rosser, T. Shpeisman, and D. Wonnacott. The Omega library (Version 1.1.0) interface guide. http:\/\/www.cs.umd.edu\/projects\/omega , Nov. 1996."},{"key":"30_CR16","series-title":"Lect Notes Comput Sci","first-page":"424","volume-title":"Proc. Computer Aided Verification","author":"Y. Kesten","year":"1997","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In O. Grumberg, editor, Proc. Computer Aided Verification, volume 1254 of LNCS, pages 424\u2013435. Springer-Verlag, June 1997."},{"key":"30_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/3-540-63166-6_13","volume-title":"Proc. Computer Aided Verification","author":"N. Klarlund","year":"1997","unstructured":"N. Klarlund. An nlogn algorithm for online BDD refinement. In O. Grumberg, editor, Proc. Computer Aided Verification, volume 1254 of LNCS, pages 107\u2013118. Springer-Verlag, June 1997."},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"A. Krishnakumar and K.-T. Cheng. On the computation of the set of reachable states of hybrid models. In Proc. 31st Design Automat. Conf., pages 615\u2013621, June 1994.","DOI":"10.1145\/196244.196583"},{"key":"30_CR19","series-title":"Lect Notes Comput Sci","first-page":"414","volume-title":"Proceedings of the REX Workshiop on Stepwise Refinement of Distribute Systems, Models, Formalisms, Correctness","author":"R. P. Kurshan","year":"1989","unstructured":"R. P. Kurshan. Analysis of discrete event coordination. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Proceedings of the REX Workshiop on Stepwise Refinement of Distribute Systems, Models, Formalisms, Correctness, volume 430 of LNCS, pages 414\u2013453. Springer-Verlag, 1989."},{"key":"30_CR20","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan and K. L. McMillan. A structural induction theorem for processes. In Proc. Eighth Symp. Princ. of Distributed Computing, pages 239\u2013247, 1989.","DOI":"10.1145\/72981.72998"},{"key":"30_CR21","volume-title":"Elements of the Theory of Computation","author":"H. R. Lewis","year":"1981","unstructured":"H. R. Lewis and C. H. Papadimitriou. Elements of the Theory of Computation. Prentice Hall Englewood Cliffs, New Jersey, 1981."},{"issue":"8","key":"30_CR22","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/135226.135233","volume":"35","author":"W. Pugh","year":"1992","unstructured":"W. Pugh. A practical algorithm for exact array dependence analysis. Communications of the ACM, 35(8):102\u2013114, Aug. 1992.","journal-title":"Communications of the ACM"},{"key":"30_CR23","series-title":"Lect Notes Comput Sci","volume-title":"Proc. Computer Aided Verification","author":"T. R. Shiple","year":"1998","unstructured":"T. R. Shiple, J. H. Kukula, and R. K. Ranjan. A comparison of Presburger engines for EFSM reachability. In A. Hu and M. Vardi, editors, Proc. Computer Aided Verification, LNCS Vancouver, June 1998. Springer-Verlag."},{"key":"30_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/3-540-60360-3_30","volume-title":"Proc. of Static Analysis Symposium","author":"P. Wolper","year":"1995","unstructured":"P. Wolper and B. Boigelot. An automata-theoretic approach to Presburger arithmetic constraints. In Proc. of Static Analysis Symposium, volume 983 of LNCS, pages 21\u201332. Springer-Verlag, Sept. 1995."},{"key":"30_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BFb0031811","volume-title":"Proc. Formal Methods in Computer-Aided Desigh","author":"Z. Zhou","year":"1996","unstructured":"Z. Zhou, X. Song, S. Tahar, E. Cemy, F. Corella, and M. Langevin. Formal verification of the island tunnel controller using multiway decision graphs. In M. Srivas and A. Camilleri, editors, Proc. Formal Methods in Computer-Aided Desigh, volume 1166 of LNCS, pages 233\u2013247. Sringer-Verlag, Nov. 1996."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49519-3_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T17:59:00Z","timestamp":1556906340000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49519-3_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651918","9783540495192"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-49519-3_30","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}