{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T21:07:40Z","timestamp":1789938460581,"version":"4.0.1"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319415390","type":"print"},{"value":"9783319415406","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41540-6_22","type":"book-chapter","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T09:34:07Z","timestamp":1468316047000},"page":"402-421","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":29,"title":["BDD-Based Boolean Functional Synthesis"],"prefix":"10.1007","author":[{"given":"Dror","family":"Fried","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lucas M.","family":"Tabajara","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,7,13]]},"reference":[{"issue":"4","key":"22_CR1","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1109\/TC.2008.165","volume":"58","author":"D Ba\u00f1eres","year":"2009","unstructured":"Ba\u00f1eres, D., Cortadella, J., Kishinevsky, M.: A recursive paradigm to solve Boolean relations. IEEE Trans. Comput. 58(4), 512\u2013527 (2009)","journal-title":"IEEE Trans. Comput."},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/11532231_27","volume-title":"Automated Deduction \u2013 CADE-20","author":"M Benedetti","year":"2005","unstructured":"Benedetti, M.: sKizzo: a suite to evaluate and certify QBFs. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 369\u2013376. Springer, Heidelberg (2005)"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: a case study. In: Proceedings of Conference on Design, Automation and Test in Europe, pp. 1188\u20131193. ACM (2007)","DOI":"10.1109\/DATE.2007.364456"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Brayton, R.K., Somenzi, F.: Minimization of Boolean relations. In: IEEE International Symposium on Circuits and Systems, pp. 738\u2013743. IEEE (1989)","DOI":"10.1109\/ISCAS.1989.100457"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010)"},{"issue":"8","key":"22_CR6","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"22_CR7","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10$$^{20}$$ states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Representing circuits more efficiently in symbolic model checking. In: Proceedings of 28th ACM\/IEEE Design Automation Conference, pp. 403\u2013407. ACM (1991)","DOI":"10.1145\/127601.127702"},{"issue":"24","key":"22_CR9","doi-asserted-by":"publisher","first-page":"3223","DOI":"10.1016\/j.disc.2006.06.014","volume":"306","author":"M Couceiro","year":"2006","unstructured":"Couceiro, M., Foldes, S., Lehtonen, E.: Composition of Post classes and normal forms of Boolean functions. Discrete Math. 306(24), 3223\u20133243 (2006)","journal-title":"Discrete Math."},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-642-14295-6_33","volume-title":"Computer Aided Verification","author":"R Ehlers","year":"2010","unstructured":"Ehlers, R.: Symbolic bounded synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 365\u2013379. Springer, Heidelberg (2010)"},{"key":"22_CR11","first-page":"309","volume":"1","author":"J Gergov","year":"1994","unstructured":"Gergov, J., Meinel, C.: Boolean manipulation with free BDDs: an application in combinational logic verification. IFIP Congr. 1, 309\u2013314 (1994)","journal-title":"IFIP Congr."},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Manolios, P.: Quantifier elimination via clause redundancy. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20\u201323 October 2013, pp. 85\u201392 (2013)","DOI":"10.1109\/FMCAD.2013.6679395"},{"issue":"4","key":"22_CR13","doi-asserted-by":"publisher","first-page":"1105","DOI":"10.2307\/2273673","volume":"48","author":"Y Gurevich","year":"1983","unstructured":"Gurevich, Y., Shelah, S.: Rabin\u2019s uniformization problem. J. Symb. Log. 48(4), 1105\u20131119 (1983)","journal-title":"J. Symb. Log."},{"key":"22_CR14","volume-title":"Logic Synthesis and Verification Algorithms","author":"GD Hachtel","year":"1996","unstructured":"Hachtel, G.D., Somenzi, F.: Logic Synthesis and Verification Algorithms. Kluwer Academic Publishers, Boston (1996)"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Heule, M., Seidl, M., Biere, A.: Efficient extraction of Skolem functions from QRAT proofs. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 21\u201324 October 2014, pp. 107\u2013114 (2014)","DOI":"10.1109\/FMCAD.2014.6987602"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-642-02658-4_30","volume-title":"Computer Aided Verification","author":"J-HR Jiang","year":"2009","unstructured":"Jiang, J.-H.R.: Quantifier elimination via functional composition. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 383\u2013397. Springer, Heidelberg (2009)"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Jiang, J.R., Lin, H., Hung, W.: Interpolating functions from large Boolean relations. In: 2009 International Conference on Computer-Aided Design (ICCAD 2009), 2\u20135 November 2009, San Jose, CA, USA, pp. 779\u2013784. IEEE (2009)","DOI":"10.1145\/1687399.1687544"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-73368-3_29","volume-title":"Computer Aided Verification","author":"B Jobstmann","year":"2007","unstructured":"Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: a tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 258\u2013262. Springer, Heidelberg (2007)"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"John, A.K., Shah, S., Chakraborty, S., Trivedi, A., Akshay, S.: Skolem functions for factored formulas. In: Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, 27\u201330 September 2015, pp. 73\u201380 (2015)","DOI":"10.1109\/FMCAD.2015.7542255"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Ganai, M., Paruthi, V.: Circuit-based Boolean reasoning. In: Proceedings of Design Automation Conference, pp. 232\u2013237. IEEE (2001)","DOI":"10.1145\/378239.378470"},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722167_12","volume-title":"Computer Aided Verification","author":"JH Kukula","year":"2000","unstructured":"Kukula, J.H., Shiple, T.R.: Building circuits from relations. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 113\u2013123. Springer, Heidelberg (2000)"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: Zorn, B.G., Aiken, A. (eds.) Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, 5\u201310 June 2010, pp. 316\u2013329. ACM (2010)","DOI":"10.1145\/1806596.1806632"},{"issue":"1\u20133","key":"22_CR23","first-page":"25","volume":"35","author":"G Pan","year":"2005","unstructured":"Pan, G., Vardi, M.Y.: Symbolic techniques in satisfiability solving. J. Autom. Reason. 35(1\u20133), 25\u201350 (2005)","journal-title":"J. Autom. Reason."},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Paruthi, V., Kuehlmann, A.: Equivalence checking combining a structural SAT-solver, BDDs, and simulation. In: Proceedings of the International Conference on Computer Design, pp. 459\u2013464. IEEE (2000)","DOI":"10.1109\/ICCD.2000.878323"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N Piterman","year":"2006","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364\u2013380. Springer, Heidelberg (2006)"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of 16th ACM Symposium on Principles of Programming Languages, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Rabbah, R.M., Bod\u00edk, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: Proceedings of the ACM Conference on Programming Language Design and Implementation, pp. 281\u2013294. ACM (2005)","DOI":"10.1145\/1064978.1065045"},{"key":"22_CR28","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package Release 2.5.0. (2012). http:\/\/vlsi.colorado.edu\/fabio\/CUDD\/"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Tronci, E.: Automatic synthesis of controllers from formal specifications. In: ICFEM, pp. 134\u2013143 (1998)","DOI":"10.1109\/ICFEM.1998.730577"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41540-6_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T00:41:32Z","timestamp":1748997692000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41540-6_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415390","9783319415406"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41540-6_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 July 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}