{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T20:10:14Z","timestamp":1736021414258,"version":"3.32.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2005,10,7]],"date-time":"2005-10-07T00:00:00Z","timestamp":1128643200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2005,10,7]],"date-time":"2005-10-07T00:00:00Z","timestamp":1128643200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2006,2]]},"DOI":"10.1007\/s10009-004-0171-8","type":"journal-article","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T10:24:17Z","timestamp":1128594257000},"page":"26-36","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Efficient BDDs for bounded arithmetic constraints"],"prefix":"10.1007","volume":"8","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":[[2005,10,7]]},"reference":[{"unstructured":"Cadence SMV. http:\/\/www-cad.eecs.berkeley.edu\/\u223ckenmcmil\/smv","key":"171_CRCSMV"},{"unstructured":"NuSMV. http:\/\/nusmv.irst.itc.it\/","key":"171_CRNuSMV"},{"unstructured":"SMV. www.cs.cmu.edu\/\u223cmodelcheck\/smv.html","key":"171_CRSMV"},{"key":"171_CRAnd91","first-page":"principles","volume":"programming","author":"Andrews","year":"1991","unstructured":"Andrews GR (1991) Concurrent programming: principles and practice. Benjamin\/Cummings, Redwood City, CA","journal-title":"Concurrent"},{"key":"171_CRBB03b","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1142\/S0129054103001911","volume":"14","author":"Bartzis","year":"2003","unstructured":"Bartzis C, Bultan T (2003) Efficient symbolic representations for arithmetic constraints in verification. Int J Found Comput Sci 14(4):605\u2013624","journal-title":"Int J Found Comput Sci"},{"doi-asserted-by":"crossref","unstructured":"Bartzis C, Bultan T (2003) Construction of efficient BDDs for bounded arithmetic constraints. In: Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol\u20092619. Springer, Berlin Heidelberg New York, pp\u2009394\u2013408","key":"171_CRBB03a","DOI":"10.1007\/3-540-36577-X_28"},{"doi-asserted-by":"crossref","unstructured":"Boudet A, Comon H (1996) Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner H","key":"#cr-split#-171_CRBC96.1","DOI":"10.1007\/3-540-61064-2_27"},{"unstructured":"(ed) Proceedings of the 21st international colloquium on trees in algebra and programming (CAAP'96), April 1996. Lecture notes in computer science, vol\u20091059. Springer, Berlin Heidelberg New York, pp\u200930-43","key":"#cr-split#-171_CRBC96.2"},{"key":"171_CRBry86","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Trans Comput 35(8):677\u2013691","journal-title":"IEEE Trans Comput"},{"doi-asserted-by":"crossref","unstructured":"Bryant RE, Chen YA (1995) Verification of arithmetic functions with binary moment diagrams. In: Proceedings of the 32nd ACM\/IEEE conference on design automation, June 1995","key":"171_CRBC95","DOI":"10.1145\/217474.217583"},{"unstructured":"Bultan T, Yavuz-Kahveci T (2001) Action Language Verifier. In: Proceedings of the 16th IEEE international conference on automated software engineering","key":"171_CRBY01"},{"key":"171_CRCAB98","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"Chan","year":"1998","unstructured":"Chan W, Anderson RJ, Beame P, Burns S, Modugno F, Notkin D, Reese JD (1998) Model checking large software specifications. IEEE Trans Softw Eng 24(7):498\u2013520","journal-title":"IEEE Trans Softw Eng"},{"doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) Nusmv 2: An opensource tool for symbolic model checking. In: Proceedings of the international conference on computer-aided verification","key":"171_CRCCG02","DOI":"10.1007\/3-540-45657-0_29"},{"doi-asserted-by":"crossref","unstructured":"Clarke EM, McMillan KL, Zhao X, Fujita M, Yang J (1993) Spectral transforms for large boolean functions with applications to technology mapping. In: Proceedings of the 30th international conference on design automation. ACM Press, New York, pp\u200954\u201360","key":"171_CRCetal93","DOI":"10.1145\/157485.164569"},{"unstructured":"Clarke EM, Fujita M, Zhao X (2000) Hybrid decision diagrams \u2013 overcoming the limitations of mtbdds and bmds. In: Proceedings of the international conference on computer-aided design, pp\u2009159\u2013163","key":"171_CRCFZ95"},{"key":"171_CRGJ79","first-page":"a","volume":"intractability","author":"Garey","year":"1979","unstructured":"Garey M, Jonson D (1979) Computers and intractability: a guide to the theory of NP-completeness. Freeman, New York","journal-title":"Computers and"},{"doi-asserted-by":"crossref","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer, Norwell, MA","key":"171_CRMcM93","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"171_CRP81","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"Papadimitriou","year":"1981","unstructured":"Papadimitriou CH (1981) On the complexity of integer programming. J ACM 28(4):765\u2013768","journal-title":"J ACM"},{"doi-asserted-by":"crossref","unstructured":"Bahar RI, Frohm EA, Gaona CM, Hachtel GD, Macii E, Pardo A, Somenzi F (1993) Algebraic Decision Diagrams and their applications. In: IEEE \/ACM international conference on computer-aided design, pp\u2009188\u2013191. IEEE Press, New York","key":"171_CRBetal93","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"171_CRSW93","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/0020-0190(93)90256-9","volume":"48","author":"Sieling","year":"1993","unstructured":"Sieling D, Wegener I (1993) Reduction of OBDDs in linear time. Inf Process Lett 48(3):139\u2013144","journal-title":"Inf Process Lett"},{"doi-asserted-by":"crossref","unstructured":"Wolper P, Boigelot B (2000) On the construction of automata from linear arithmetic constraints. In: Graf S, Schwartzbach M (eds) Proceedings of the 6th international conference on tools and algorithms for the construction and analysis of systems, April 2000. Lecture notes in computer science, vol 1785. Springer, Berlin Heidelberg New York, pp\u20091\u201319","key":"171_CRWB00","DOI":"10.1007\/3-540-46419-0_1"},{"key":"171_CRYMW97","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1145\/244795.244803","volume":"19","author":"Yang","year":"1997","unstructured":"Yang J, Mok AK, Wang F (1997) Symbolic model checking for event-driven real-time systems. ACM Trans Programm Lang Syst 19(2):386\u2013412","journal-title":"ACM Trans Programm Lang Syst"},{"unstructured":"Yavuz-Kahveci T, Tuncer M, Bultan T (2001) Composite symbolic library. In: Proceedings of the 7th international conference on tools and algorithms for the construction and analysis of systems, April 2001. Lecture notes in computer science, vol\u20092031. Springer, Berlin Heidelberg New York, pp\u2009335\u2013344","key":"171_CRYTB01"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0171-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-004-0171-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0171-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0171-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T19:56:57Z","timestamp":1736020617000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-004-0171-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,10,7]]},"references-count":23,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,2]]}},"alternative-id":["171"],"URL":"https:\/\/doi.org\/10.1007\/s10009-004-0171-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2005,10,7]]},"assertion":[{"value":"7 October 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}