{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:55:11Z","timestamp":1725551711362},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540237389"},{"type":"electronic","value":"9783540304944"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30494-4_30","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T14:42:14Z","timestamp":1277822534000},"page":"430-444","source":"Crossref","is-referenced-by-count":0,"title":["Variable Reuse for Efficient Image Computation"],"prefix":"10.1007","author":[{"given":"Zijiang","family":"Yang","sequence":"first","affiliation":[]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the 36th ACM\/IEEE Design Automation Conference, pp. 317\u2013320 (1999)","key":"30_CR1","DOI":"10.1145\/309847.309942"},{"key":"30_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Eighth International Conference on Computer Aided Verification","author":"R. Brayton","year":"1996","unstructured":"Brayton, R., Hachtel, G., Sangiovanni-Vincentell, A., Somenzi, F., Aziz, A., Cheng, S., Edwards, S., Khatri, S., Kukimoto, Y., Pardo, A., Qadeer, S., Ranjan, R., Sarwary, S., Shiple, T., Swamy, G., Villa, T.: VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102. Springer, Heidelberg (1996)"},{"doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean-function manipulation. IEEE Transactions on Computers\u00a0C-35(8) (1986)","key":"30_CR3","DOI":"10.1109\/TC.1986.1676819"},{"issue":"2","key":"30_CR4","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., Dill, D.L., Hwang, L.J., McMillan, K.L.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: Proceedings of the IFIP International Conference on Very Large Scale Integration: VLSI 1991, pp. 49\u201358 (1991)","key":"30_CR5"},{"key":"30_CR6","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., Jha, S., Kukula, J., Veith, H., Wang, D.: Using combinatorial optimization methods for quantifier scheduling. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 293\u2013309. Springer, Heidelberg (2001)"},{"unstructured":"Chauhan, P., Clarke, E.M., Jha, S., Kukula, J., Shiple, T., Veith, H., Wong, D.: Non-linear quantification scheduling in image computation. In: Proceedings of the International Conference on Computer Aided Design: ICCAD 2001 (2001)","key":"30_CR7"},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proc. Workshop on Logic of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc. Workshop on Logic of Programs. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1981)"},{"key":"30_CR9","volume-title":"Model checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (2000)"},{"issue":"6","key":"30_CR10","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/6.499951","volume":"33","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Kurshan, R.P.: Computer-aided verification. IEEE Spectrum\u00a033(6), 61\u201367 (1996)","journal-title":"IEEE Spectrum"},{"key":"30_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/3-540-58179-0_63","volume-title":"Computer Aided Verification","author":"D. Geist","year":"1994","unstructured":"Geist, D., Beer, I.: Efficient model checking by automated ordering of transition relation partitions. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 299\u2013310. Springer, Heidelberg (1994)"},{"key":"30_CR12","volume-title":"Algorithmic Graph Theory and Perfect Graph","author":"M. Golumbic","year":"1980","unstructured":"Golumbic, M.: Algorithmic Graph Theory and Perfect Graph. Academic Press, London (1980)"},{"key":"30_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/3-540-40922-X_22","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Gupta","year":"2000","unstructured":"Gupta, A., Yang, Z., Ashar, P., Gupta, A.: SAT-based image computation with applications in reachability analysis. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 354\u2013371. Springer, Heidelberg (2000)"},{"key":"30_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"Computer Aided Verification","author":"R. Hardin","year":"1996","unstructured":"Hardin, R., Har\u2019El, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 423\u2013427. Springer, Heidelberg (1996)"},{"key":"30_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking: an approach to the state explosion problem","author":"K. McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic model checking: an approach to the state explosion problem. Kluwer Academic Publishers, Dordrecht (1993)"},{"doi-asserted-by":"crossref","unstructured":"Moon, I.-H., Kukula, J.H., Ravi, K., Somenzi, F.: To split or to conjoin: the question in image computation. In: Proceedings of the 37th Design Automation Conference, pp. 26\u201328 (2000)","key":"30_CR16","DOI":"10.1145\/337292.337305"},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/3-540-40922-X_6","volume-title":"Formal Methods in Computer-Aided Design","author":"I.-H. Moon","year":"2000","unstructured":"Moon, I.-H., Somenzi, F.: Border-block traingular form and conjunction schedule in image computation. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 73\u201390. Springer, Heidelberg (2000)"},{"unstructured":"Ranjan, R., Aziz, A., Plessier, B., Pixley, C., Brayton, R.: Efficient BDD algorithms for FSM synthesis and verification. In: Proceedings of the IEEE\/ACM International Workshop on Logic Synthesis (1995)","key":"30_CR18"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30494-4_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T15:26:18Z","timestamp":1558279578000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30494-4_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540237389","9783540304944"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30494-4_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}