{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:07:16Z","timestamp":1736399236372,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540330561"},{"type":"electronic","value":"9783540330578"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11691372_8","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T14:22:26Z","timestamp":1143555746000},"page":"120-134","source":"Crossref","is-referenced-by-count":3,"title":["Efficient Guided Symbolic Reachability Using Reachability Expressions"],"prefix":"10.1007","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","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-45069-6_13","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2003","unstructured":"Beyer, D., Lewerentz, C., Noack, A.: Rabbit: A tool for BDD-based verification of real-time systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 122\u2013125. Springer, Heidelberg (2003)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Symbolic guided search for CTL model checking. In: Proceeding of ACM\/IEEE DAC, pp. 29\u201334 (2000)","DOI":"10.1145\/337292.337306"},{"issue":"8","key":"8_CR3","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 Transactions on Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"8_CR4","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 ICCAD, pp. 293\u2013298 (2001)","DOI":"10.1109\/ICCAD.2001.968636"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/3-540-44798-9_24","volume-title":"Correct Hardware Design and Verification Methods","author":"P. Chauhan","year":"2001","unstructured":"Chauhan, P., Clarke, E.M., Jha, S., Kukula, J., Veith, H., Wang, D.: Using combinatorial optimization methods for quantification scheduling. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 293\u2013309. Springer, Heidelberg (2001)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","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 checkin. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"8_CR7","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 LICS, pp. 1\u201333 (1990)"},{"key":"8_CR8","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 ICCAD, pp. 388\u2013393 (1997)","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"8_CR9","unstructured":"Pandya, P.K., Raut, M.: A kleene algebra of reachability expressions and its use in efficient symbolic guided search. Technical Report (in preparation), STCS, Tata Institute of Fundamental Research (2005)"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"D. Thomas, S. Chakraborty, and P. K. Pandya. Efficient guided symbolic reachability using reachability expressions. Technical Report TR-06-1, CFDVS, IIT Bombay (January 2006)","DOI":"10.1007\/11691372_8"},{"key":"8_CR11","unstructured":"Thomas, D., Pandya, P.K., Chakraborty, S.: Scheduling clusters in model checking of real time systems. Technical Report TR-04-16, CFDVS, IIT Bombay (September 2004), http:\/\/www.cfdvs.iitb.ac.in\/reports\/techrep04.php3"}],"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\/11691372_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,8]],"date-time":"2025-01-08T04:53:37Z","timestamp":1736312017000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11691372_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540330561","9783540330578"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/11691372_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}