{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:50:10Z","timestamp":1762458610880,"version":"3.33.0"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2008,1,8]],"date-time":"2008-01-08T00:00:00Z","timestamp":1199750400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transf"],"published-print":{"date-parts":[[2008,3]]},"DOI":"10.1007\/s10009-007-0057-7","type":"journal-article","created":{"date-parts":[[2008,1,7]],"date-time":"2008-01-07T07:38:16Z","timestamp":1199691496000},"page":"113-129","source":"Crossref","is-referenced-by-count":4,"title":["Efficient guided symbolic reachability using reachability expressions"],"prefix":"10.1007","volume":"10","author":[{"given":"Dina","family":"Thomas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Supratik","family":"Chakraborty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paritosh","family":"Pandya","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,1,8]]},"reference":[{"key":"57_CR1","doi-asserted-by":"crossref","unstructured":"Beyer, D., Lewerentz, C., Noack, A.: Rabbit: a tool for BDD-based verification of real-time systems. In: Proceedings of International Conference on Computer-Aided Verification. Lecture Notes in Computer Science, vol. 2727, pp. 122\u2013125. Springer, Heidelberg (2003)","DOI":"10.1007\/978-3-540-45069-6_13"},{"key":"57_CR2","doi-asserted-by":"crossref","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Symbolic guided search for CTL model checking. In: Proceedings of ACM\/IEEE Design Automation Conference, pp. 29\u201334. ACM Press, New York (2000)","DOI":"10.1145\/337292.337306"},{"key":"57_CR3","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35(8), 677\u2013691. IEEE CS Press, Washington DC (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"57_CR4","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Sequential circuit verification using symbolic model checking. In: Proceedings of ACM\/IEEE Design Automation Conference, pp. 46\u201361. ACM Press, New York (1990)","DOI":"10.1145\/123186.123223"},{"key":"57_CR5","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Camurati, P., Lavagno, L., Quer, S.: Disjunctive partitioning and partial iterative squaring: an effective approach for symbolic traversal of large circuits. In: Proceedings of ACM\/IEEE Design Automation Conference, pp. 728\u2013733. ACM Press, New York (1997)","DOI":"10.1145\/266021.266355"},{"key":"57_CR6","doi-asserted-by":"crossref","unstructured":"Chauhan, P., Clarke, E.M., Jha, S., Kukula, J., Shiple, T., Veith, H., Wang, D.: Non-linear quantification scheduling in image computation. In: Proceedings of ACM\/IEEE International Conference on Computer-Aided Design, pp. 293\u2013298. IEEE Press, Piscataway (2001)","DOI":"10.1109\/ICCAD.2001.968636"},{"key":"57_CR7","doi-asserted-by":"crossref","unstructured":"Chauhan, P., Clarke, E.M., Jha, S., Kukula, J., Veith, H., Wang, D.: Using combinatorial optimization methods for quantification scheduling. In: Proceedings of the Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), Lecture Notes in Computer Science, vol. 2144, pp. 293\u2013309. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-44798-9_24"},{"key":"57_CR8","doi-asserted-by":"crossref","unstructured":"Chung, M.-Y., Ciardo, G., Yu, A.J.: A fine-grained fullness-guided chaining heuristic for symbolic reachability analysis. In: Proceedings of the International Symposium on Automated Technology for Verification and Analysis, Lecture Notes in Computer Science, vol. 4218, pp. 51\u201366. Springer, Heidelberg (2006)","DOI":"10.1007\/11901914_7"},{"key":"57_CR9","doi-asserted-by":"crossref","unstructured":"Ciardo, G.,Marmorstein, R., Siminiceanu, R.: The saturation algorithm for symbolic state-space exploration. Int. J. Softw. Tools Technol. Transf.8(1), 4\u201325. Springer, Heidelberg (2006)","DOI":"10.1007\/s10009-005-0188-7"},{"key":"57_CR10","doi-asserted-by":"crossref","unstructured":"Ciardo, G., Yu, A.J.: Saturation-based symbolic reachability analysis using conjunctive and disjunctive partitioning. In: Proceedings of the Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), Lecture Notes in Computer Science, vol. 3725, pp. 146\u2013161. Springer, Heidelberg (2005)","DOI":"10.1007\/11560548_13"},{"key":"57_CR11","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV version 2: An opensource tool for symbolic model checking. In: Proceedings of International Conference on Computer-Aided Verification, Lecture Notes in Computer Science, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"57_CR12","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: Proceedings of IEEE Symposium on Logic In Computer Science, pp. 1\u201333. IEEE CS Press, Washington DC (1990)"},{"key":"57_CR13","doi-asserted-by":"crossref","unstructured":"Narayan, A., Isles, A.J., Jain, J., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Reachability analysis using partitioned-ROBDDs. In: Proceedings of ACM\/IEEE Internationl Conference on Computer-Aided Design, pp. 388\u2013393. IEEE CS Press, Washington DC (1997)","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"57_CR14","doi-asserted-by":"crossref","unstructured":"Roig, O., Cortadella, J., Pastor, E.: Verification of asynchronous circuits by BDD-based model checking of petri nets. In: Proceedings of the International Conference on Application and Theory of Petri Nets, Lecture Notes in Computer Science, vol. 815, pp. 374\u2013391. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-60029-9_50"},{"key":"57_CR15","unstructured":"Thomas, D., Chakraborty, S., Pandya, P.K.: Efficient guided symbolic reachability using reachability expressions. Technical Report TR-06-19. http:\/\/www.cfdvs.iitb.ac.in\/reports\/techrep06.php3 , CFDVS, IIT Bombay (2006)"},{"key":"57_CR16","unstructured":"Thomas, D., Pandya, P.K., Chakraborty, S.: Scheduling clusters in model checking of real time systems. Technical Report TR-04-16. http:\/\/www.cfdvs.iitb.ac.in\/reports\/techrep04.php3 , CFDVS, IIT Bombay (2004)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-007-0057-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-007-0057-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-007-0057-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,25]],"date-time":"2025-01-25T10:44:08Z","timestamp":1737801848000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-007-0057-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1,8]]},"references-count":16,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,3]]}},"alternative-id":["57"],"URL":"https:\/\/doi.org\/10.1007\/s10009-007-0057-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2008,1,8]]}}}