{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,5]],"date-time":"2026-04-05T10:18:13Z","timestamp":1775384293392,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540665595","type":"print"},{"value":"9783540481539","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48153-2_14","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:13:28Z","timestamp":1269897208000},"page":"172-187","source":"Crossref","is-referenced-by-count":8,"title":["Abstract BDDs: A Technique for Using Abstraction in Model Checking"],"prefix":"10.1007","author":[{"given":"Edmund","family":"Clarke","sequence":"first","affiliation":[]},{"given":"Somesh","family":"Jha","sequence":"additional","affiliation":[]},{"given":"Yuan","family":"Lu","sequence":"additional","affiliation":[]},{"given":"Dong","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant, \u201cGraph-Based Algorithms for Boolean Function Manipulation\u201d, IEEE Trans. on Comput., Vol. C-35, No. 8, pp. 677\u2013691, Aug. 1986.","journal-title":"IEEE Trans. on Comput."},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill, \u201cSymbolic Model Checking for Sequential Circuit Verification\u201d, IEEE Trans. on CAD of Integrated Circuits and System, Vol.13, No.4, pp.401-424, 1994.","DOI":"10.1109\/43.275352"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla, \u201cAutomatic verification of finitestate concurrent system using temporal logic\u201d, Proceedings of the Tenth Annual ACM Symposium on Principles of Programming Languages (POPL), January, 1983.","DOI":"10.1145\/567067.567080"},{"issue":"1\/2","key":"14_CR4","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E. M. Clarke","year":"1996","unstructured":"E. M. Clarke, R. Enders, T. Filkorn and S. Jha, \u201cExploiting Symmetry in Temporal Logic Model Checking\u201d, Formal Methods in System Design 9(1\/2):77\u2013104, 1996.","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"14_CR5","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/BF01383968","volume":"6","author":"E. M. Clarke","year":"1995","unstructured":"E. M. Clarke and O. Grumberg and H. Hiraishi and S. Jha and D. E. Long and K. L. McMillan and L. A. Ness, \u201cVerification of the Futurebus+ Cache Coherence Protocol\u201d, Formal Methods in System Design 6(2):217\u2013232, 1995.","journal-title":"Formal Methods in System Design"},{"key":"14_CR6","unstructured":"E. M. Clarke, O. Grumberg, D. E. Long, \u201cModel Checking and Abstraction\u201d, ACM Transactions on Programming Languages and System (TOPLAS), Vol. 16, No. 5, pp. 1512\u20131542, Sept. 1994."},{"issue":"1\/2","key":"14_CR7","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E. A. Emerson","year":"1996","unstructured":"E. A. Emerson and A. P. Sistla, \u201cSymmetry and Model Checking\u201d, Formal Methods in System Design 9(1\/2):105\u2013130, 1996.","journal-title":"Formal Methods in System Design"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"P. Godefroid, D. Peled, and M. Staskauskas, \u201cUsing Partial Order Methods in the Formal Verification of Industrial Concurrent Programs\u201d, ISSTA'96 International Symposium on Software Testing and Analysis, pp. 261\u2013269, San Diego, California, USA, 1996. ACM Press.","DOI":"10.1145\/229000.226324"},{"key":"14_CR9","unstructured":"J. L. Hennessy, D. A. Patterson, Computer Architecture: A Quantitative Approach, second edition, 1996. Morgan Kaufman Press."},{"issue":"1\/2","key":"14_CR10","first-page":"41","volume":"9","author":"C. N. Ip","year":"1996","unstructured":"C. N. Ip and D. L. Dill, \u201cBetter Verification Through Symmetry\u201d, Formal Methods in System Design 9(1\/2):41\u201376, 1996.","journal-title":"Formal Methods in System Design"},{"key":"14_CR11","unstructured":"S. Jha, Y. Lu, M. Minea, E. M. Clarke, \u201cEquivalence Checking using Abstract BDDs\u201d, Intl. Conf. on Computer Design (ICCD), 1997."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Shinji Kimura, \u201cResidue BDD and Its Application to the Verification of Arithmetic Circuits\u201d, 32nd Design Automation Conference (DAC), 1995.","DOI":"10.1145\/217474.217584"},{"key":"14_CR13","unstructured":"D. E. Long, \u201cModel Checking, Abstraction and Compositional Verification\u201d, School of Computer Science, Carnegie Mellon University publication CMU-CS-93-178, July 1993."},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"K. L. McMillan, \u201cSymbolic Model Checking: An Approach to the State Explosion Problem\u201d. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"D. Peled, \u201cCombining Partial Order Reduction with on-the-fly model-checking\u201d, Journal of Formal Methods in System Design, 8(1):39\u201364.","DOI":"10.1007\/BF00121262"},{"key":"14_CR16","unstructured":"PCI SGI, \u201cPCI Local Bus Specification\u201d, Production Version Revision 2.1, June 1, 1995."},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Kavita Ravi, Abelardo Pardo, Gary D. Hachtel, Fabio Somenzi, \u201cModular Verification of Multipliers\u201d, Formal Methods in Computer-Aided Design, pp. 49\u201363, Nov. 1996.","DOI":"10.1007\/BFb0031799"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48153-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T18:59:04Z","timestamp":1558983544000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665595","9783540481539"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}