{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:40:03Z","timestamp":1739994003383,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_28","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"394-408","source":"Crossref","is-referenced-by-count":8,"title":["Construction of Efficient BDDs for Bounded Arithmetic Constraints"],"prefix":"10.1007","author":[{"given":"Constantinos","family":"Bartzis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"28_CR1","unstructured":"Cadence SMV. http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/smv ."},{"key":"28_CR2","volume-title":"Concurrent Programming: Principles and Practice","author":"G. R. Andrews","year":"1991","unstructured":"G. R. Andrews. Concurrent Programming: Principles and Practice. The Benjamin\/ Cummings Publishing Company, Redwood City, California, 1991."},{"key":"28_CR3","unstructured":"R. Bryant. Graph-based algorithms for boolean function manipulation. In Proceedings of the 27th ACM\/IEEE Design Automation Conference, 1990."},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"R.E Bryant and Y.A. Chen. Verification of arithmetic functions with binary moment diagrams. In Proceedings of the 32nd ACM\/IEEE Design Automation Conference, June 1995.","DOI":"10.1145\/217474.217583"},{"issue":"1","key":"28_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/332740.332746","volume":"9","author":"T. Bultan","year":"2000","unstructured":"T. Bultan, R. Gerber, and C. League. Composite model checking: Verification with type-specific symbolic representations. ACM Transactions on Software Engineering and Methodology, 9(1):3\u201350, January 2000.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"T. Bultan and T. Yavuz-Kahveci. Action language verifier. In Proceedings of the 16th IEEE International Conference on Automated Software Engineering, 2001.","DOI":"10.1109\/ASE.2001.989834"},{"issue":"7","key":"28_CR7","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"W. Chan","year":"1998","unstructured":"W. Chan, R. J. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. D. Reese. Model checking large software specifications. IEEE Transactions on Software Engineering, 24(7):498\u2013520, July 1998.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"A. Cimatti, E.M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. Nusmv 2: An opensource tool for symbolic model checking. In Proceedings of the International Conference on Computer-Aided Verification, 2002.","DOI":"10.1007\/3-540-45657-0_29"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, M. Fujita, and X. Zhao. Hybrid decision diagrams-overcoming the limitations of mtbdds and bmds. In In International Conference of Computer-Aided Design, pages 159\u2013163, 2000.","DOI":"10.1109\/ICCAD.1995.480007"},{"key":"28_CR10","unstructured":"M. Garey and D. Jonson. Computers and Intractability: A Guide to the Theory of NP-completeness. Freeman, 1979."},{"key":"28_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"K. L. McMillan","year":"1993","unstructured":"K. L. McMillan. Symbolic model checking. Kluwer Academic Publishers, Massachusetts, 1993."},{"issue":"2","key":"28_CR12","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1145\/244795.244803","volume":"19","author":"J. Yang","year":"1997","unstructured":"J. Yang, A. K. Mok, and F. Wang. Symbolic model checking for event-driven real-time systems. ACM Transactions on Programming Languages and Systems, 19(2):386\u2013412, March 1997.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"28_CR13","series-title":"Lect Notes Comput Sci","first-page":"335","volume-title":"Composite symbolic library","author":"T. Yavuz-Kahveci","year":"2001","unstructured":"T. Yavuz-Kahveci, M. Tuncer, and T. Bultan. Composite symbolic library. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of Lecture Notes in Computer Science, pages 335\u2013344. Springer-Verlag, April 2001."}],"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\/3-540-36577-X_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:10:16Z","timestamp":1739992216000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_28","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}