{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T19:10:44Z","timestamp":1736277044287,"version":"3.32.0"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2006,1]]},"DOI":"10.1007\/s10703-006-4617-3","type":"journal-article","created":{"date-parts":[[2006,2,9]],"date-time":"2006-02-09T00:15:00Z","timestamp":1139444100000},"page":"5-36","source":"Crossref","is-referenced-by-count":6,"title":["Compositional SCC Analysis for Language Emptiness"],"prefix":"10.1007","volume":"28","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[]},{"given":"Roderick","family":"Bloem","sequence":"additional","affiliation":[]},{"given":"Gary D.","family":"Hachtel","sequence":"additional","affiliation":[]},{"given":"Kavita","family":"Ravi","sequence":"additional","affiliation":[]},{"given":"Fabio","family":"Somenzi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4617_CR1","doi-asserted-by":"crossref","unstructured":"F. Balarin and A.L. Sangiovanni-Vincentelli, \u201cAn iterative approach to language containment,\u201d in C. Courcoubetis, editor, Fifth Conference on Computer Aided Verification (CAV '93). Springer-Verlag, Berlin, 1993. LNCS 697.","DOI":"10.1007\/3-540-56922-7_4"},{"key":"4617_CR2","doi-asserted-by":"crossref","unstructured":"R. Bloem, H. N. Gabow, and F. Somenzi, \u201cAn algorithm for strongly connected component analysis in n log n symbolic steps,\u201d in W.A. Hunt, Jr. and S.D. Johnson (Eds.), Formal Methods in Computer Aided Design, LNCS 1954, Springer-Verlag, pp. 37\u201354, November 2000.","DOI":"10.1007\/3-540-40922-X_4"},{"key":"4617_CR3","unstructured":"R. Bloem, H.N. Gabow, and F. Somenzi, \u201cAn algorithm for strongly connected component analysis in n log n symbolic steps,\u201d Formal Methods in System Design, Vol. 27, No. 2, 2005 (To appear)."},{"key":"4617_CR4","doi-asserted-by":"crossref","unstructured":"R. Bloem, K. Ravi, and F. Somenzi, \u201cEfficient decision procedures for model checking of linear time logic properties,\u201d in N. Halbwachs and D. Peled (Eds.), Eleventh Conference on Computer Aided Verification (CAV'99), Springer-Verlag, Berlin, LNCS 1633, 1999, pp. 222\u2013235.","DOI":"10.1007\/3-540-48683-6_21"},{"key":"4617_CR5","doi-asserted-by":"crossref","unstructured":"R.K. Brayton et al. \u201cVIS: A system for verification and synthesis,\u201d in T. Henzinger and R. Alur (Eds.), Eighth Conference on Computer Aided Verification (CAV'96), Springer-Verlag, Rutgers University, LNCS 1102, 1996, pp. 428\u2013432.","DOI":"10.1007\/3-540-61474-5_95"},{"issue":"8","key":"4617_CR6","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, \u201cGraph-based algorithms for Boolean function manipulation,\u201d IEEE Transactions on Computers, Vol. C-35, No. 8, pp. 677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"4617_CR7","doi-asserted-by":"crossref","unstructured":"P. Chauhan, E. Clarke, J. Kukula, S. Sapra, H. Veith, and D. Wang, \u201cAutomated abstraction refinement for model checking large state spaces using SAT based conflict analysis,\u201d in M. D. Aagaard and J. W. O'Leary (Eds.), Formal Methods in Computer Aided Design, Springer-Verlag, LNCS 2517, 2002, pp. 33\u201351.","DOI":"10.1007\/3-540-36126-X_3"},{"key":"4617_CR8","doi-asserted-by":"crossref","unstructured":"H. Cho, G. D. Hachtel, E. Macii, M. Poncino, and F. Somenzi, \u201cA state space decomposition algorithm for approximate FSM traversal,\u201d in Proceedings of the European Conference on Design Automation, Paris, France, 1994, pp. 137\u2013141.","DOI":"10.1145\/157485.164555"},{"key":"4617_CR9","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, \u201cCounterexample-guided abstraction refinement,\u201d in E.A. Emerson and A.P. Sistla (Eds.), Twelfth Conference on Computer Aided Verification (CAV'00), Berlin, LNCS 1855, Springer-Verlag, pp. 154\u2013169, 2000.","DOI":"10.1007\/10722167_15"},{"key":"4617_CR10","doi-asserted-by":"crossref","unstructured":"E. Clarke, A. Gupta, J. Kukula, and O. Strichman, \u201cSAT based abstraction-refinement using ILP and machine learning,\u201d in E. Brinksma and K.G. Larsen (Eds.), Fourteenth Conference on Computer Aided Verification (CAV'02), LNCS 2404, Springer-Verlag, pp. 265\u2013279, 2002.","DOI":"10.1007\/3-540-45657-0_20"},{"key":"4617_CR11","unstructured":"O. Coudert, C. Berthet, and J.C. Madre, \u201cVerification of sequential machines using Boolean functional vectors,\u201d in L. Claesen (Ed.), Proceedings IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Leuven, Belgium, pp. 111\u2013128, 1989."},{"key":"4617_CR12","doi-asserted-by":"crossref","unstructured":"O. Coudert and J. C. Madre, \u201cA unified framework for the formal verification of sequential circuits,\u201d in Proceedings of the IEEE International Conference on Computer Aided Design, 1990, pp. 126\u2013129.","DOI":"10.1109\/ICCAD.1990.129859"},{"key":"4617_CR13","unstructured":"E. A. Emerson and C. -L. Lei, \u201cEfficient model checking in fragments of the propositional mu-calculus,\u201d in Proceedings of the First Annual Symposium of Logic in Computer Science, 1986, pp. 267\u2013278."},{"key":"4617_CR14","doi-asserted-by":"crossref","unstructured":"K. Fisler, R. Fraer, G. Kamhi, M. Vardi, and Z. Yang, \u201cIs there a best symbolic cycle-detection algorithm?\u201d in T. Margaria and W. Yi (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2031, Springer-Verlag, pp. 420\u2013434, 2001.","DOI":"10.1007\/3-540-45319-9_29"},{"key":"4617_CR15","unstructured":"R. Gentilini, C. Piazza, and A. Policriti, \u201cComputing strongly connected componenets in a linear number of symbolic steps,\u201d in Symposium on Discrete Algorithms, Baltimore, MD, 2003."},{"key":"4617_CR16","doi-asserted-by":"crossref","unstructured":"A. Gupta, M. Ganai, Z. Yang, and P. Ashar, \u201cIterative abstraction using SAT-based BMC with proof analysis,\u201d in Proceedings of the International Conference on Computer-Aided Design, 2003, pp. 416\u2013423.","DOI":"10.1109\/ICCAD.2003.1257811"},{"key":"4617_CR17","doi-asserted-by":"crossref","unstructured":"R. Hojati, H. Touati, R. P. Kurshan, and R. K. Brayton, \u201cEfficient \u03c9-regular language containment,\u201d in Computer Aided Verification, Montr\u00e9al, Canada, 1992, pp. 371\u2013382.","DOI":"10.1007\/3-540-56496-9_31"},{"key":"4617_CR18","unstructured":"J.-Y. Jang, \u201cIterative abstraction-based CTL model checking,\u201d PhD thesis, University of Colorado, Department of Electrical and Computer Engineering, 1999."},{"key":"4617_CR19","doi-asserted-by":"crossref","unstructured":"Y. Kesten, A. Pnueli, and L.-O. Raviv, \u201cAlgorithmic verification of linear temporal logic specifications,\u201d in International Colloquium on Automata, Languages, and Programming (ICALP-98), LNCS 1443, Berlin, Springer, pp. 1\u201316, 1998.","DOI":"10.1007\/BFb0055036"},{"key":"4617_CR20","unstructured":"O. Kupferman and M. Y. Vardi, \u201cFreedom, weakness, and determinism: From linear-time to branching-time,\u201d in Proc. 13th IEEE Symposium on Logic in Computer Science, 1998."},{"key":"4617_CR21","volume-title":"Computer-Aided Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1994","unstructured":"R.P. Kurshan, Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994."},{"key":"4617_CR22","unstructured":"W. Lee, A. Pardo, J. Jang, G. Hachtel, and F. Somenzi, \u201cTearing based abstraction for CTL model checking,\u201d in Proceedings of the International Conference on Computer-Aided Design, San Jose, CA, 1996, pp. 76\u201381."},{"issue":"7","key":"4617_CR23","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/s10009-004-0169-2","volume":"2","author":"B. Li","year":"2005","unstructured":"B. Li, C. Wang, and F. Somenzi, \u201cAbstraction refinement in symbolic model checking using satisfiability as the only decision procedure,\u201d Software Tools for Technology Transfer, Vol. 2, No. 7, pp. 143\u2013155, 2005.","journal-title":"Software Tools for Technology Transfer"},{"key":"4617_CR24","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli, \u201cChecking that finite state concurrent programs satisfy their linear specification,\u201d in Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, New Orleans, 1985, pp. 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"4617_CR25","doi-asserted-by":"crossref","unstructured":"J. Lind-Nielsen, H.R. Andersen, G. Behrmann, H. Hulgaard, K. Kristoffersen, and K.G. Larsen, \u201cVerification of large state\/event systems using compositionality and dependency analysis,\u201d in International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'98), Lisbon, Portugal, LNCS 1384, 1998, pp. 201\u2013216.","DOI":"10.1007\/BFb0054173"},{"key":"4617_CR26","volume-title":"Symbolic Model Checking","author":"K. L. McMillan","year":"1994","unstructured":"K. L. McMillan. Symbolic Model Checking, Kluwer Academic Publishers, Boston, MA, 1994."},{"key":"4617_CR27","doi-asserted-by":"crossref","unstructured":"K. L. McMillan and N. Amla, \u201cAutomatic abstraction without counterexamples,\u201d in International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'03), Warsaw, Poland, LNCS 2619, 2003, pp. 2\u201317.","DOI":"10.1007\/3-540-36577-X_2"},{"key":"4617_CR28","unstructured":"R. Milner, \u201cAn algebraic definition of simulation between programs,\u201d in Proc. 2nd Int. Joint Conf. on Artificial Intelligence, 1971, pp. 481\u2013489."},{"key":"4617_CR29","doi-asserted-by":"crossref","unstructured":"I.-H. Moon, J.-Y. Jang, G.D. Hachtel, F. Somenzi, C. Pixley, and J. Yuan, \u201cApproximate reachability don't cares for CTL model checking,\u201d in Proceedings of the International Conference on Computer-Aided Design, San Jose, CA, 1998, pp. 351\u2013358.","DOI":"10.1145\/288548.289053"},{"key":"4617_CR30","doi-asserted-by":"crossref","unstructured":"A. Pardo and G. D. Hachtel, \u201cAutomatic abstraction techniques for propositional \u03bc-calculus model checking,\u201d in O. Grumberg (Ed.), Ninth Conference on Computer Aided Verification (CAV'97), Springer-Verlag, Berlin, LNCS 1254, 1997, pp. 12\u201323.","DOI":"10.1007\/3-540-63166-6_5"},{"key":"4617_CR31","doi-asserted-by":"crossref","unstructured":"A. Pardo and G. D. Hachtel, \u201cIncremental CTL model checking using BDD subsetting,\u201d in Proceedings of the Design Automation Conference, San Francisco, CA, 1998, pp. 457\u2013462.","DOI":"10.1145\/277044.277171"},{"key":"4617_CR32","doi-asserted-by":"crossref","unstructured":"K. Ravi, R. Bloem, and F. Somenzi, \u201cA comparative study of symbolic algorithms for the computation of fair cycles,\u201d in W.A. Hunt, Jr. and S.D. Johnson (Eds.), Formal Methods in Computer Aided Design, Springer-Verlag, 2000. LNCS 1954, pp. 143\u2013160.","DOI":"10.1007\/3-540-40922-X_10"},{"key":"4617_CR33","doi-asserted-by":"crossref","unstructured":"K. Ravi and F. Somenzi, \u201cHigh-density reachability analysis,\u201d in Proceedings of the International Conference on Computer-Aided Design, San Jose, CA, 1995, pp. 154\u2013158.","DOI":"10.1109\/ICCAD.1995.480006"},{"key":"4617_CR34","doi-asserted-by":"crossref","unstructured":"F. Somenzi, K. Ravi, and R. Bloem, \u201cAnalysis of symbolic SCC hull algorithms,\u201d in M.D. Aagaard and J.W. O'Leary (Eds.), Formal Methods in Computer Aided Design, Springer-Verlag, LNCS 2517, pp. 88\u2013105, 2002.","DOI":"10.1007\/3-540-36126-X_6"},{"issue":"1","key":"4617_CR35","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1006\/inco.1995.1055","volume":"118","author":"H. J. Touati","year":"1995","unstructured":"H. J. Touati, R. K. Brayton, and R. P. Kurshan, \u201cTesting language containment for \u03c9-automata using BDD's,\u201d Information and Computation, Vol. 118, No. 1, pp. 101\u2013109, 1995.","journal-title":"Information and Computation"},{"key":"4617_CR36","unstructured":"M. Y. Vardi and P. Wolper, \u201cAn automata-theoretic approach to automatic program verification,\u201d in Proceedings of the First Symposium on Logic in Computer Science, Cambridge, UK, 1986, pp. 322\u2013331."},{"key":"4617_CR37","unstructured":"URL: http:\/\/vlsi.colorado.edu\/vis."},{"key":"4617_CR38","doi-asserted-by":"crossref","unstructured":"C. Wang, R. Bloem, G. D. Hachtel, K. Ravi, and F. Somenzi. \u201cDivide and compose: SCC refinement for language emptiness,\u201d in International Conference on Concurrency Theory (CONCUR01), Berlin, Springer-Verlag, LNCS 2154, August 2001, pp. 456\u2013471.","DOI":"10.1007\/3-540-44685-0_31"},{"key":"4617_CR39","doi-asserted-by":"crossref","unstructured":"C. Wang and G. D. Hachtel, \u201cSharp disjunctive decomposition for language emptiness checking,\u201d in M. D. Aagaard and J. W. O'Leary, (Eds.), Formal Methods in Computer Aided Design, Springer-Verlag, LNCS 2517, November 2002, pp. 105\u2013122.","DOI":"10.1007\/3-540-36126-X_7"},{"key":"4617_CR40","unstructured":"C. Wang, B. Li, H. Jin, G. D. Hachtel, and F. Somenzi, \u201cImproving Ariadne's bundle by following multiple threads in abstraction refinement,\u201d in Proceedings of the International Conference on Computer-Aided Design, November 2003, pp. 408\u2013415."},{"key":"4617_CR41","doi-asserted-by":"crossref","unstructured":"D. Wang, P.-H. Ho, J. Long, J. Kukula, Y. Zhu, T. Ma, and R. Damiano, \u201cFormal property verification by abstraction refinement with formal, simulation and hybrid engines,\u201d in Proceedings of the Design Automation Conference, Las Vegas, NV, June 2001, pp. 35\u201340.","DOI":"10.1145\/378239.378260"},{"issue":"10","key":"4617_CR42","doi-asserted-by":"crossref","first-page":"1225","DOI":"10.1109\/43.875347","volume":"19","author":"A. Xie","year":"2000","unstructured":"A. Xie and P. A. Beerel, \u201cImplicit enumeration of strongly connected components and an application to formal verification,\u201d IEEE Transactions on Computer-Aided Design, Vol. 19, No. 10, pp. 1225\u20131230, 2000.","journal-title":"IEEE Transactions on Computer-Aided Design"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-4617-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-4617-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-4617-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T18:00:17Z","timestamp":1736272817000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-4617-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,1]]}},"alternative-id":["4617"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-4617-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2006,1]]}}}