{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T21:40:40Z","timestamp":1740260440326,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_30","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"435-449","source":"Crossref","is-referenced-by-count":3,"title":["A Mechanically Verified AIG-to-BDD Conversion Algorithm"],"prefix":"10.1007","author":[{"given":"Sol","family":"Swords","sequence":"first","affiliation":[]},{"suffix":"Jr.","given":"Warren A.","family":"Hunt","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"30_CR1","doi-asserted-by":"crossref","unstructured":"Aagaard, M.D., Jones, R.B., Seger, C.-J.H.: Formal verification using parametric representations of boolean constraints. In: Proceedings of the 36th Design Automation Conference, pp. 402\u2013407 (1999)","DOI":"10.1145\/309847.309968"},{"key":"30_CR2","doi-asserted-by":"crossref","unstructured":"Berman, C.L., Trevillyan, L.H.: Functional comparison of logic designs for VLSI circuits. In: IEEE International Conference on Computer-Aided Design, November 5-9, pp. 456\u2013459 (1989)","DOI":"10.1109\/ICCAD.1989.76990"},{"key":"30_CR3","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1145\/1217975.1217992","volume-title":"ACL \u201906: Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications","author":"R.S. Boyer","year":"2006","unstructured":"Boyer, R.S., Hunt Jr, W.A.: Function memoization and unique object representation for ACL2 functions. In: ACL \u201906: Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications, pp. 81\u201389. ACM, New York (2006)"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/3-540-63475-4_1","volume-title":"Formal Hardware Verification","author":"S. Hazelhurst","year":"1997","unstructured":"Hazelhurst, S., Seger, C.-J.H.: Symbolic trajectory evaluation. In: Kropf, T. (ed.) Formal Hardware Verification. LNCS, vol.\u00a01287, pp. 3\u201378. Springer, Heidelberg (1997)"},{"key":"30_CR5","series-title":"Lecture Notes in Computer Science","first-page":"353","volume-title":"CAV 2009","author":"W.A. Hunt Jr.","year":"2009","unstructured":"Hunt Jr., W.A., Swords, S.: Centaur technology media unit verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 353\u2013367. Springer, Heidelberg (2009)"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Moore, J.S., Boyer, R.S.: ACL2 version 3.3 (2008), http:\/\/www.cs.utexas.edu\/~moore\/acl2\/","DOI":"10.1016\/j.jal.2007.07.002"},{"key":"30_CR7","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Moore, J.S., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000)"},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Ganai, M.K., Paruthi, V.: Circuit-based boolean reasoning. In: Proceedings of the 38th Design Automation Conference, pp. 232\u2013237 (2001)","DOI":"10.1145\/378239.378470"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Krohm, F.: Equivalence checking using cuts and heaps. In: Proceedings of the 34th Design Automation Conference, June 9-13, pp. 263\u2013268 (1997)","DOI":"10.1145\/266021.266090"},{"key":"30_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-36126-X_1","volume-title":"Formal Methods in Computer-Aided Design","author":"T.F. Melham","year":"2002","unstructured":"Melham, T.F., Jones, R.B.: Abstraction by symbolic indexing transformations. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 1\u201318. Springer, Heidelberg (2002)"},{"issue":"9","key":"30_CR11","doi-asserted-by":"publisher","first-page":"1381","DOI":"10.1109\/TCAD.2005.850814","volume":"24","author":"C.-J.H. Seger","year":"2005","unstructured":"Seger, C.-J.H., Jones, R.B., O\u2019Leary, J.W., Melham, T., Aagaard, M.D., Barrett, C., Syme, D.: An industrially effective environment for formal hardware verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a024(9), 1381\u20131405 (2005)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"30_CR12","unstructured":"Somenzi, F.: CUDD: CU decision diagram package release 2.4.1 (2005), http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T21:14:28Z","timestamp":1740258868000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}