{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T01:40:01Z","timestamp":1750988401427,"version":"3.41.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319672946"},{"type":"electronic","value":"9783319672953"}],"license":[{"start":{"date-parts":[[2017,11,16]],"date-time":"2017-11-16T00:00:00Z","timestamp":1510790400000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-67295-3_7","type":"book-chapter","created":{"date-parts":[[2017,11,15]],"date-time":"2017-11-15T12:36:44Z","timestamp":1510749404000},"page":"151-168","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Analysis of Incomplete Circuits Using Dependency Quantified Boolean Formulas"],"prefix":"10.1007","author":[{"given":"Ralf","family":"Wimmer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karina","family":"Wimmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Scholl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,11,16]]},"reference":[{"key":"7_CR1","unstructured":"P. Ashar, M.K. Ganai, A. Gupta, F. Ivancic, Z. Yang, Efficient SAT-based bounded model checking for software verification, in International Symposium on Leveraging Applications of Formal Methods (ISoLA), ed. by T. Margaria, B. Steffen, A. Philippou, M. Reitenspie\u00df, Technical Report, Paphos, Cyprus, vol. TR-2004-6 (Department of Computer Science, University of Cyprus, 2004), pp. 157\u2013164"},{"key":"7_CR2","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1016\/j.tcs.2013.12.020","volume":"523","author":"V Balabanov","year":"2014","unstructured":"V. Balabanov, H.-J. Katherine Chiang, J.-H.R. Jiang, Henkin quantifiers and Boolean formulae: a certification perspective of DQBF. Theor. Comput. Sci. 523, 86\u2013100 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR3","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"A. Biere, A. Cimatti, E.M. Clarke, O. Strichman, Y. Zhu, Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"R. Bloem, R. K\u00f6nighofer, M. Seidl, SAT-based synthesis methods for safety specs, in Proceedings of VMCAI, ed. by K.L. McMillan, X. Rival. Lecture Notes in Computer Science, San Diego, CA, vol. 8318 (Springer, Berlin, 2014 ), pp. 1\u201320","DOI":"10.1007\/978-3-642-54013-4_1"},{"key":"7_CR5","unstructured":"R. Bloem, U. Egly, P. Klampfl, R. K\u00f6nighofer, F. Lonsing, M. Seidl, Satisfiability-based methods for reactive synthesis from safety specifications. CoRR, abs\/1604.06204 (2016), http:\/\/arxiv.org\/abs\/1604.06204"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"R.K. Brayton, A. Mishchenko, ABC: an academic industrial-strength verification tool, in Proceedings of CAV, ed. by T. Touili, B. Cook, P. Jackson. Lecture Notes in Computer Science, Edinburgh, vol. 6174 (Springer, Berlin, 2010), pp. 24\u201340","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"7_CR7","unstructured":"U. Bubeck, Model-based transformations for quantified Boolean formulas. PhD thesis, University of Paderborn (2010)"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"U. Bubeck, H. Kleine B\u00fcning, Dependency quantified Horn formulas: models and complexity, in Proceedings of SAT, ed. by A. Biere, C.P. Gomes. Lecture Notes in Computer Science, Seattle, WA, vol. 4121 (Springer, Berlin, 2006), pp. 198\u2013211","DOI":"10.1007\/11814948_21"},{"issue":"1","key":"7_CR9","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"E.M. Clarke, A. Biere, R. Raimi, Y. Zhu, Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"7_CR10","first-page":"151","volume-title":"The complexity of theorem-proving procedures, in Proceedings of STOC","author":"SA Cook","year":"1971","unstructured":"S.A. Cook, The complexity of theorem-proving procedures, in Proceedings of STOC (ACM, New York, 1971), pp. 151\u2013158"},{"issue":"3\u20134","key":"7_CR11","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/s10766-009-0124-7","volume":"38","author":"A Czutro","year":"2010","unstructured":"A. Czutro, I. Polian, M.D.T. Lewis, P. Engelke, S.M. Reddy, B. Becker, Thread-parallel integrated test pattern generator utilizing satisfiability analysis. Int. J. Parallel Prog. 38(3\u20134),185\u2013202 (2010)","journal-title":"Int. J. Parallel Prog."},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"W. Damm, B. Finkbeiner, Automatic compositional synthesis of distributed systems, in Proceedings of FM, ed. by C.B. Jones, P. Pihlajasaari, J. Sun. Lecture Notes in Computer Science, Singapore, vol. 8442 (Springer, Berlin, 2014), pp. 179\u2013193","DOI":"10.1007\/978-3-319-06410-9_13"},{"issue":"4","key":"7_CR13","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1109\/MDT.2012.2205479","volume":"29","author":"S Eggersgl\u00fc\u00df","year":"2012","unstructured":"S. Eggersgl\u00fc\u00df, R. Drechsler, A highly fault-efficient SAT-based ATPG flow. IEEE Des. Test Comput. 29(4), 63\u201370 (2012)","journal-title":"IEEE Des. Test Comput."},{"issue":"5\u20136","key":"7_CR14","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"B. Finkbeiner, S. Schewe, Bounded synthesis. Int. J. Softw. Tools Technol. Transfer 15(5\u20136), 519\u2013539 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"B. Finkbeiner, L. Tentrup, Fast DQBF refutation, in Proceedings of SAT, ed. by C. Sinz, U. Egly. Lecture Notes in Computer Science, Vienna, vol. 8561 (Springer, Berlin, 2014), pp. 243\u2013251","DOI":"10.1007\/978-3-319-09284-3_19"},{"key":"7_CR16","volume-title":"A DPLL algorithm for solving DQBF, in International Workshop on Pragmatics of SAT (POS), Trento","author":"A Fr\u00f6hlich","year":"2012","unstructured":"A. Fr\u00f6hlich, G. Kov\u00e1sznai, A. Biere, A DPLL algorithm for solving DQBF, in International Workshop on Pragmatics of SAT (POS), Trento (2012)"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"A. Fr\u00f6hlich, G. Kov\u00e1sznai, A. Biere, H. Veith, iDQ: instantiation-based DQBF solving, in International Workshop on Pragmatics of SAT (POS), ed. by D. Le Berre. EPiC Series, Vienna, vol. 27 ( EasyChair, 2014), pp. 103\u2013116","DOI":"10.29007\/1s5k"},{"key":"7_CR18","first-page":"61","volume-title":"Proceedings of MBMV","author":"K Gitina","year":"2013","unstructured":"K. Gitina, S. Reimer, M. Sauer, R. Wimmer, C. Scholl, B. Becker, Equivalence checking for partial implementations revisited, in Proceedings of MBMV, ed. by C. Haubelt, D. Timmermann, Rostock (Universit\u00e4t Rostock, ITMZ, 2013), pp. 61\u201370"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"K. Gitina, S. Reimer, M. Sauer, R. Wimmer, C. Scholl, B. Becker, Equivalence checking of partial designs using dependency quantified Boolean formulae, in Proceedings of ICCD, Asheville, NC (IEEE CS, 2013), pp. 396\u2013403","DOI":"10.1109\/ICCD.2013.6657071"},{"key":"7_CR20","volume-title":"Solving DQBF through quantifier elimination, in Proceedings of DATE, Grenoble","author":"K Gitina","year":"2015","unstructured":"K. Gitina, R. Wimmer, S. Reimer, M. Sauer, C. Scholl, B. Becker, Solving DQBF through quantifier elimination, in Proceedings of DATE, Grenoble (IEEE, New York, 2015)"},{"key":"7_CR21","first-page":"37","volume-title":"Advanced SAT-techniques for bounded model checking of blackbox designs, in Proceedings of MTV","author":"M Herbstritt","year":"2006","unstructured":"M. Herbstritt, B. Becker, C. Scholl, Advanced SAT-techniques for bounded model checking of blackbox designs, in Proceedings of MTV (IEEE, New York, 2006), pp. 37\u201344"},{"issue":"2\u20133","key":"7_CR22","first-page":"71","volume":"7","author":"F Lonsing","year":"2010","unstructured":"F. Lonsing, A. Biere, DepQBF: a dependency-aware QBF solver. J. Satisf. Boolean Model. Comput. 7(2\u20133), 71\u201376 (2010)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"F. Lonsing, F. Bacchus, A. Biere, U. Egly, M. Seidl, Enhancing search-based QBF solving by dynamic blocked clause elimination, in Proceedings of LPAR, ed. by M. Davis, A. Fehnker, A. McIver, A. Voronkov. Lecture Notes in Computer Science, Suva, vol. 9450 (Springer, Berlin, 2015), pp. 418\u2013433","DOI":"10.1007\/978-3-662-48899-7_29"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Applications of Craig interpolants in model checking, in Proceedings of TACAS, ed. by N. Halbwachs, L.D. Zuck. Lecture Notes in Computer Science, Edinburgh, vol. 3440 (Springer, Berlin, 2005), pp. 1\u201312","DOI":"10.1007\/978-3-540-31980-1_1"},{"issue":"6","key":"7_CR25","doi-asserted-by":"crossref","first-page":"1234","DOI":"10.1109\/TC.2012.53","volume":"62","author":"T Nopper","year":"2013","unstructured":"T. Nopper, C. Scholl, Symbolic model checking for incomplete designs with flexible modeling of unknowns. IEEE Trans. Comput. 62(6), 1234\u20131254 (2013)","journal-title":"IEEE Trans. Comput."},{"issue":"7\u20138","key":"7_CR26","doi-asserted-by":"crossref","first-page":"957","DOI":"10.1016\/S0898-1221(00)00333-3","volume":"41","author":"G Peterson","year":"2001","unstructured":"G. Peterson, J. Reif, S. Azhar, Lower bounds for multiplayer non-cooperative games of incomplete information. Comput. Math. Appl. 41(7\u20138), 957\u2013992 (2001)","journal-title":"Comput. Math. Appl."},{"key":"7_CR27","first-page":"1596","volume-title":"Exploiting structure in an AIG based QBF solver, in Proceedings of DATE","author":"F Pigorsch","year":"2009","unstructured":"F. Pigorsch, C. Scholl, Exploiting structure in an AIG based QBF solver, in Proceedings of DATE (IEEE, New York, 2009), pp. 1596\u20131601"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"A. Pnueli, R. Rosner, Distributed reactive systems are hard to synthesize, in Annual Symposium on Foundations of Computer Science, St. Louis, MO (IEEE Computer Society, Washington, 1990), pp. 746\u2013757","DOI":"10.1109\/FSCS.1990.89597"},{"key":"7_CR29","first-page":"238","volume-title":"Checking equivalence for partial implementations, in Proceedings of DAC, Las Vegas, NV","author":"C Scholl","year":"2001","unstructured":"C. Scholl, B. Becker, Checking equivalence for partial implementations, in Proceedings of DAC, Las Vegas, NV (ACM, New York, 2001), pp. 238\u2013243"},{"issue":"2","key":"7_CR30","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/BF01383966","volume":"6","author":"C-JH Seger","year":"1995","unstructured":"C.-J.H. Seger, R.E. Bryant, Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods Syst. Des. 6(2), 147\u2013189 (1995)","journal-title":"Formal Methods Syst. Des."},{"issue":"9","key":"7_CR31","doi-asserted-by":"crossref","first-page":"1381","DOI":"10.1109\/TCAD.2005.850814","volume":"24","author":"C-JH Seger","year":"2005","unstructured":"C.-J.H. Seger, R.B. Jones, J.W. O\u2019Leary, T.F. Melham, M. Aagaard, C. Barrett, D. Syme, An industrially effective environment for formal hardware verification. IEEE Trans. CAD Integr. Circuits Syst. 24(9), 1381\u20131405 (2005)","journal-title":"IEEE Trans. CAD Integr. Circuits Syst."},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"G.S. Tseitin, On the complexity of derivation in propositional calculus, in Studies in Constructive Mathematics and Mathematical Logic Part 2 (Springer, Berlin, 1970), pp. 115\u2013125","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"R. Wimmer, K. Gitina, J. Nist, C. Scholl, B. Becker, Preprocessing for DQBF, in Proceedings of SAT, ed. by M. Heule, S. Weaver. Lecture Notes in Computer Science, Austin, TX, vol. 9340 (Springer, Berlin, 2015), pp. 173\u2013190","DOI":"10.1007\/978-3-319-24318-4_13"},{"key":"7_CR34","first-page":"395","volume-title":"Skolem functions for DQBF, in Proceedings of ATVA, Lecture Notes in Computer Science, Chiba","author":"K Wimmer","year":"2016","unstructured":"K. Wimmer, R. Wimmer, C. Scholl, B. Becker, Skolem functions for DQBF, in Proceedings of ATVA, Lecture Notes in Computer Science, Chiba, vol. 9938 (Springer, Berlin, 2016), pp. 395\u2013411"},{"key":"7_CR35","volume-title":"Skolem functions for DQBF (extended version)","author":"K Wimmer","year":"2016","unstructured":"K. Wimmer, R. Wimmer, C. Scholl, B. Becker, Skolem functions for DQBF (extended version). Technical Report, FreiDok, Freiburg im Breisgau (2016), https:\/\/www.freidok.uni-freiburg.de\/data\/11130"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"R. Wimmer, S. Reimer, P. Marin, B. Becker, HQSpre\u2013an effective preprocessor for QBF and DQBF, in Proceedings of TACAS, Part I, ed. by A. Legay, T. Margaria. Lecture Notes in Computer Science, Uppsala, vol. 10205 (Springer, Berlin, 2017)","DOI":"10.1007\/978-3-662-54577-5_21"}],"container-title":["Advanced Logic Synthesis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67295-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,27]],"date-time":"2025-06-27T00:59:07Z","timestamp":1750985947000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67295-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,16]]},"ISBN":["9783319672946","9783319672953"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67295-3_7","relation":{},"subject":[],"published":{"date-parts":[[2017,11,16]]}}}