{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:24:13Z","timestamp":1725891853875},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540472377"},{"type":"electronic","value":"9783540472384"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901914_7","type":"book-chapter","created":{"date-parts":[[2006,10,10]],"date-time":"2006-10-10T01:21:43Z","timestamp":1160443303000},"page":"51-66","source":"Crossref","is-referenced-by-count":5,"title":["A Fine-Grained Fullness-Guided Chaining Heuristic for Symbolic Reachability Analysis"],"prefix":"10.1007","author":[{"given":"Ming-Ying","family":"Chung","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gianfranco","family":"Ciardo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andy Jinqing","family":"Yu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"8","key":"7_CR1","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comp.\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comp."},{"key":"7_CR2","series-title":"IFIP Transactions","first-page":"49","volume-title":"Proc. Int. Conference on Very Large Scale Integration","author":"J.R. Burch","year":"1991","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: Proc. Int. Conference on Very Large Scale Integration, August 1991. IFIP Transactions, pp. 49\u201358. North-Holland, Amsterdam (1991)"},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1016\/j.peva.2005.06.001","volume":"63","author":"G. Ciardo","year":"2006","unstructured":"Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.: Logical and stochastic modeling with SMART. Perf. Eval.\u00a063, 578\u2013608 (2006)","journal-title":"Perf. Eval."},{"key":"7_CR4","unstructured":"Ciardo, G., Lan, Y.: Faster discrete-event simulation through structural caching. In: Proc. PMCCS, September 2003, pp. 11\u201314 (2003)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-44988-4_8","volume-title":"Application and Theory of Petri Nets 2000","author":"G. Ciardo","year":"2000","unstructured":"Ciardo, G., L\u00fcttgen, G., Ciardo, G., Siminiceanu, R.: Efficient symbolic state-space construction for asynchronous systems. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol.\u00a01825, pp. 103\u2013122. Springer, Heidelberg (2000)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/3-540-45319-9_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Ciardo","year":"2001","unstructured":"Ciardo, G., L\u00fcttgen, G., Siminiceanu, R.: Saturation: An efficient iteration strategy for symbolic state space generation. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 328\u2013342. Springer, Heidelberg (2001)"},{"issue":"1","key":"7_CR7","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/s10009-005-0188-7","volume":"8","author":"G. Ciardo","year":"2006","unstructured":"Ciardo, G., Marmorstein, R., Siminiceanu, R.: The saturation algorithm for symbolic state space exploration. STTT\u00a08(1), 4\u201325 (2006)","journal-title":"STTT"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-540-45069-6_4","volume-title":"Computer Aided Verification","author":"G. Ciardo","year":"2003","unstructured":"Ciardo, G., Siminiceanu, R.: Structural symbolic CTL model checking of asynchronous systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 40\u201353. Springer, Heidelberg (2003)"},{"issue":"1","key":"7_CR9","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/0166-5316(93)90026-Q","volume":"18","author":"G. Ciardo","year":"1993","unstructured":"Ciardo, G., Trivedi, K.S.: A decomposition approach for stochastic reward net models. Perf. Eval.\u00a018(1), 37\u201359 (1993)","journal-title":"Perf. Eval."},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/11560548_13","volume-title":"Correct Hardware Design and Verification Methods","author":"G. Ciardo","year":"2005","unstructured":"Ciardo, G., Yu, A.J.: Saturation-based symbolic reachability analysis using conjunctive and disjunctive partitioning. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 146\u2013161. Springer, Heidelberg (2005)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)"},{"issue":"3","key":"7_CR12","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1145\/278298.278303","volume":"45","author":"P. Fernandes","year":"1998","unstructured":"Fernandes, P., Plateau, B., Stewart, W.J.: Efficient descriptor-vector multiplication in stochastic automata networks. J. ACM\u00a045(3), 381\u2013414 (1998)","journal-title":"J. ACM"},{"key":"7_CR13","first-page":"150","volume-title":"Proc. FOCS","author":"A. Itai","year":"1981","unstructured":"Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. In: Proc. FOCS, pp. 150\u2013158. IEEE Comp. Soc. Press, Los Alamitos (October 1981)"},{"issue":"1\u20132","key":"7_CR14","first-page":"9","volume":"4","author":"T. Kam","year":"1998","unstructured":"Kam, T., Villa, T., Brayton, R., Sangiovanni-Vincentelli, A.: Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic\u00a04(1\u20132), 9\u201362 (1998)","journal-title":"Multiple-Valued Logic"},{"key":"7_CR15","first-page":"220","volume-title":"Proc. ICCD","author":"S. Kimura","year":"1990","unstructured":"Kimura, S., Clarke, E.M.: A parallel algorithm for constructing binary decision diagrams. In: Proc. ICCD, pp. 220\u2013223. IEEE Computer Society Press, Los Alamitos (1990)"},{"key":"7_CR16","unstructured":"Martin, A.J.: The design of a self-timed circuit for distributed mutual exclusion. In: Proc. Chapel Hill Conference on VLSI, pp. 245\u2013260 (1985)"},{"key":"7_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer, Dordrecht (1993)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/3-540-48745-X_2","volume-title":"Application and Theory of Petri Nets 1999","author":"A.S. Miner","year":"1999","unstructured":"Miner, A.S., Ciardo, G.: Efficient reachability set generation and storage using decision diagrams. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol.\u00a01639, pp. 6\u201325. Springer, Heidelberg (1999)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1007\/3-540-58152-9_23","volume-title":"Application and Theory of Petri Nets 1994","author":"E. Pastor","year":"1994","unstructured":"Pastor, E., Roig, O., Cortadella, J., Badia, R.: Petri net analysis using boolean manipulation. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol.\u00a0815, pp. 416\u2013435. Springer, Heidelberg (1994)"},{"key":"7_CR20","first-page":"154","volume-title":"Proc. ICCAD","author":"K. Ravi","year":"1995","unstructured":"Ravi, K., Somenzi, F.: High-density reachability analysis. In: Proc. ICCAD, pp. 154\u2013158. IEEE Comp. Soc. Press, Los Alamitos (1995)"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-48153-2_19","volume-title":"Correct Hardware Design and Verification Methods","author":"K. Ravi","year":"1999","unstructured":"Ravi, K., Somenzi, F.: Hints to accelerate Symbolic Traversal. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 250\u2013266. Springer, Heidelberg (1999)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1007\/3-540-60029-9_50","volume-title":"Application and Theory of Petri Nets 1995","author":"O. Roig","year":"1995","unstructured":"Roig, O., Cortadella, J., Pastor, E.: Verification of asynchronous circuits by BDD-based model checking of Petri nets. In: DeMichelis, G., D\u00edaz, M. (eds.) ICATPN 1995. LNCS, vol.\u00a0935, pp. 374\u2013391. Springer, Heidelberg (1995)"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"R. \u00a0Siminiceanu and G.\u00a0Ciardo. New metrics for static variable ordering in decision diagrams. Proc. TACAS, LNCS 2031, pages 328\u2013342. Springer, March 2006.","DOI":"10.1007\/11691372_6"},{"key":"7_CR24","unstructured":"Tilgner, M., Takahashi, Y., Ciardo, G.: SNS 1.0: Synchronized Network Solver. In: Proc. 1st Int. Workshop on Manuf. and Petri Nets, pp. 215\u2013234 (June 1996)"},{"key":"7_CR25","unstructured":"The VIS Group: VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/11560548_17","volume-title":"Correct Hardware Design and Verification Methods","author":"D. Ward","year":"2005","unstructured":"Ward, D., Somenzi, F.: Automatic Generation of Hints for Symbolic Traversal. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 207\u2013221. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901914_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T14:56:16Z","timestamp":1605624976000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901914_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540472377","9783540472384"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11901914_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}