{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:00:09Z","timestamp":1725487209157},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540418658"},{"type":"electronic","value":"9783540453192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45319-9_29","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T15:50:47Z","timestamp":1184601047000},"page":"420-434","source":"Crossref","is-referenced-by-count":39,"title":["Is There a Best Symbolic Cycle-Detection Algorithm?"],"prefix":"10.1007","author":[{"given":"Kathi","family":"Fisler","sequence":"first","affiliation":[]},{"given":"Ranan","family":"Fraer","sequence":"additional","affiliation":[]},{"given":"Gila","family":"Kamhi","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]},{"given":"Zijiang","family":"Yang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"key":"29_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Intl. Conf. on Formal Methods in Computer-Aided Verification","author":"R. Bloem","year":"2000","unstructured":"Bloem, R., H. N. Gabow and F. Somenzi. An algorithm for strongly connected component analysis in n log n symbolic steps. In Intl. Conf. on Formal Methods in Computer-Aided Verification, Lecture Notes in Computer Science. Springer-Verlag, 2000."},{"key":"29_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/3-540-48683-6_21","volume-title":"Intl. Conf. on Computer-Aided Verification","author":"R. Bloem","year":"1999","unstructured":"Bloem, R., K. Ravi and F. Somenzi. Effcient decision procedures for model checking of linear time logic properties. In Intl. Conf. on Computer-Aided Verification, Lecture Notes in Computer Science, pages 222\u2013235. Springer-Verlag, 1999."},{"issue":"2","key":"29_CR3","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"Clarke, E. M., E. A. Emerson and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, January 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"29_CR4","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., M. Y. Vardi, P. Wolper and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275\u2013288, 1992.","journal-title":"Formal Methods in System Design"},{"key":"29_CR5","unstructured":"Emerson, E. A. and C. L. Lei. Efficient model checking in fragments of the propositional model mu-calculus. Proceedings of LICS 1986, pages 267\u2013278, 1986."},{"key":"29_CR6","unstructured":"Fraer, R., G. Kamhi, L. Fix and M. Y. Vardi. Evaluating semi-exhausting verification techniques for bug hunting. In Proceedings of the 1st Intl. Workshop on Symbolic Model Checking. Electronic Notes in Theoretical Computer Science, 1999."},{"key":"29_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"Intl. Conf. on Computer-Aided Verification","author":"R. H. Hardin","year":"1996","unstructured":"Hardin, R. H., Z. Har\u2019El and R. P. Kurshan. COSPAN. In Intl. Conf. on Computer-Aided Verification, number 1102 in Lecture Notes in Computer Science, pages 423\u2013427. Springer-Verlag, 1996."},{"key":"29_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/3-540-63166-6_27","volume-title":"Proc. Conf. on Computer-Aided verification (CAV\u201997)","author":"R. H. Hardin","year":"1997","unstructured":"Hardin, R. H., R. P. Kurshan, S. K. Shukla and M. Y. Vardi. A new heuristic for bad cycle detection using BDDs. In Proc. Conf. on Computer-Aided verification (CAV\u201997), pages 268\u2013278. Springer-Verlag. LNCS 1254, 1997."},{"key":"29_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/BFb0028745","volume-title":"Intl. Conf. on Computer-Aided Verification","author":"T. Henzinger","year":"1998","unstructured":"Henzinger, T., O. Kupferman and S. Qadeer. From prehistoric to postmodern symbolic model checking. In Hu, A. and M. Vardi, editors, Intl. Conf. on Computer-Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 195\u2013206. Springer-Verlag, 1998."},{"key":"29_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Intl. Conf. on Computer-Aided Verification","author":"R. Hojati","year":"1992","unstructured":"Hojati, R., H. Touati, R. Kurshan and R. Brayton. Efficient \u03c9-regular language containment. In Intl. Conf. on Computer-Aided Verification, number 663 in Lecture Notes in Computer Science. Springer-Verlag, 1992."},{"key":"29_CR11","series-title":"Lect Notes Comput Sci","first-page":"385","volume-title":"Intl. Conf. on Computer-Aided Verification","author":"G. Holzmann","year":"1996","unstructured":"Holzmann, G. and D. Peled. The state of SPIN. In Intl. Conf. on Computer-Aided Verification, number 1102 in Lecture Notes in Computer Science, pages 385\u2013389. Springer-Verlag, 1996."},{"key":"29_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-49519-3_19","volume-title":"Intl. Conf. on Formal Methods in Computer-Aided Verification","author":"G. Kamhi","year":"1998","unstructured":"Kamhi, G., L. Fix and Z. Binyamini. Symbolic model checking visualization. In Intl. Conf. on Formal Methods in Computer-Aided Verification, number 1522 in Lecture Notes in Computer Science, pages 290\u2013303. Springer-Verlag, 1998."},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"Karp, R. M. The transitive closure of a random digraph. Random Structures and Algorithms, 1(1), 1990.","DOI":"10.1002\/rsa.3240010106"},{"key":"29_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055036","volume-title":"Intl. Colloquium on Automata, Languages, and Programming","author":"Y. Kesten","year":"1998","unstructured":"Kesten, Y., A. Pnueli and L. on Raviv. Algorithmic verification of linear temporal logic specifications. In Intl. Colloquium on Automata, Languages, and Programming, number 1443 in Lecture Notes in Computer Science. Springer-Verlag, 1998."},{"key":"29_CR15","doi-asserted-by":"crossref","unstructured":"Kupferman, O. and M. Y. Vardi. Freedom, weakness, and determinism: From linear-time to branching-time. In IEEE Symp on Logic in Computer Science, 1998.","DOI":"10.1109\/LICS.1998.705645"},{"key":"29_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Intl. Conf. on Formal Methods in Computer-Aided Verification","author":"K. Ravi","year":"2000","unstructured":"Ravi, K., R. Bloem and F. Somenzi. A comparative study of symbolic algorithms for the computation of fair cycles. In Intl. Conf. on Formal Methods in Computer-Aided Verification, Lecture Notes in Computer Science. Springer-Verlag, 2000."},{"key":"29_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Intl. Conf. on Computer-Aided Verification","author":"The VIS Group","year":"1996","unstructured":"The VIS Group. VIS: A system for verification and synthesis. In Alur, R. and T. Henzinger, editors, Intl. Conf. on Computer-Aided Verification, volume 1102 of Lecture Notes in Computer Science. Springer-Verlag, July 1996."},{"key":"29_CR18","unstructured":"Vardi, M. Y. and P. Wolper. An automata-theoretic approach to automatic program verification. In IEEE Symposium on Logic in Computer Science, 1986."},{"key":"29_CR19","unstructured":"Yang, Z. Performance analysis of symbolic reachability algorithms in model checking. Master\u2019s thesis, Rice University, Department of Computer Science, 1999. Available at \n                    http:\/\/www.cs.rice.edu\/CS\/Verification\/\n                    \n                  ."}],"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\/3-540-45319-9_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T23:24:33Z","timestamp":1550445873000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45319-9_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418658","9783540453192"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45319-9_29","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}