{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:33:16Z","timestamp":1762101196248},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642221095"},{"type":"electronic","value":"9783642221101"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22110-1_17","type":"book-chapter","created":{"date-parts":[[2011,7,4]],"date-time":"2011-07-04T09:08:45Z","timestamp":1309770525000},"page":"191-207","source":"Crossref","is-referenced-by-count":18,"title":["Existential Quantification as Incremental SAT"],"prefix":"10.1007","author":[{"given":"J\u00f6rg","family":"Brauer","sequence":"first","affiliation":[]},{"given":"Andy","family":"King","sequence":"additional","affiliation":[]},{"given":"Jael","family":"Kriener","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Aloul, F.A., Markov, I.L., Sakallah, K.A.: Faster SAT and Smaller BDDs via Common Function Structure. In: ICCAD, pp. 443\u2013448 (2001)","DOI":"10.1109\/ICCAD.2001.968669"},{"issue":"1","key":"17_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0167-6423(96)00039-1","volume":"31","author":"T. Armstrong","year":"1998","unstructured":"Armstrong, T., Marriott, K., Schachte, P., S\u00f8ndergaard, H.: Two Classes of Boolean Functions for Dependency Analysis. Sci.\u00a0Comp.\u00a0Program.\u00a031(1), 3\u201345 (1998)","journal-title":"Sci.\u00a0Comp.\u00a0Program."},{"issue":"1","key":"17_CR3","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.entcs.2010.09.003","volume":"267","author":"E. Barrett","year":"2010","unstructured":"Barrett, E., King, A.: Range and Set Abstraction Using SAT. Electronic Notes in Theoretical Computer Science\u00a0267(1), 17\u201327 (2010)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"17_CR4","volume-title":"Canonical expressions in Boolean algebra","author":"A. Blake","year":"1938","unstructured":"Blake, A.: Canonical expressions in Boolean algebra. University of Chicago, Chicago (1938)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-15769-1_11","volume-title":"Static Analysis","author":"J. Brauer","year":"2010","unstructured":"Brauer, J., King, A.: Automatic abstraction for intervals using boolean formulae. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 167\u2013183. Springer, Heidelberg (2010)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-20398-5_7","volume-title":"NASA Formal Methods","author":"J. Brauer","year":"2011","unstructured":"Brauer, J., King, A.: Approximate quantifier elimination for propositional boolean formulae. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 73\u201388. Springer, Heidelberg (2011)"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The mathSAT\u00a04 SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 299\u2013303. Springer, Heidelberg (2008)"},{"issue":"4","key":"17_CR8","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1109\/TCAD.1987.1270310","volume":"6","author":"R. Bryant","year":"1987","unstructured":"Bryant, R.: Boolean analysis of MOS circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a06(4), 634\u2013649 (1987)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-540-69850-0_9","volume-title":"25 Years of Model Checking","author":"R.E. Bryant","year":"2008","unstructured":"Bryant, R.E.: A view from the engine room: Computational support for symbolic model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp. 145\u2013149. Springer, Heidelberg (2008), http:\/\/www.slidefinder.net\/m\/mc25\/7464626"},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098, 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"17_CR11","first-page":"69","volume-title":"FMCAD","author":"R. Cavada","year":"2007","unstructured":"Cavada, R., Cimatti, A., Franz\u00e9n, A., Kalyanasundaram, K., Roveri, M., Shyamasundar, R.K.: Computing predicate abstractions by integrating BDDs and SMT solvers. In: FMCAD, pp. 69\u201376. IEEE Computer Society Press, Los Alamitos (2007)"},{"key":"17_CR12","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1145\/996566.996711","volume-title":"DAC","author":"P. Chauhan","year":"2004","unstructured":"Chauhan, P., Clarke, E.M., Kroening, D.: A SAT-based algorithm for reparameterization in symbolic simulation. In: DAC, pp. 524\u2013529. ACM Press, New York (2004)"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-540-24605-3_7","volume-title":"Theory and Applications of Satisfiability Testing","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Talupur, M., Veith, H., Wang, D.: SAT based predicate abstraction for hardware verification. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 78\u201392. Springer, Heidelberg (2004)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-642-12002-2_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Cook","year":"2010","unstructured":"Cook, B., Kroening, D., R\u00fcmmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 236\u2013250. Springer, Heidelberg (2010)"},{"key":"17_CR15","first-page":"36","volume-title":"DAC","author":"O. Coudert","year":"1992","unstructured":"Coudert, O., Madre, J.C.: Implicit and Incremental Computation of Primes and Essential Primes of Boolean Functions. In: DAC, pp. 36\u201339. IEEE Computer Society Press, Los Alamitos (1992)"},{"key":"17_CR16","doi-asserted-by":"crossref","first-page":"818","DOI":"10.1145\/775832.776039","volume-title":"DAC","author":"R.F. Damiano","year":"2003","unstructured":"Damiano, R.F., Kukula, J.H.: Checking satisfiability of a conjunction of BDDs. In: DAC, pp. 818\u2013823. ACM Press, New York (2003)"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"issue":"1-4","key":"17_CR18","first-page":"1","volume":"2","author":"N. E\u00e9n","year":"2006","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Translating Pseudo-Boolean Constraints into SAT. JSAT\u00a02(1-4), 1\u201326 (2006)","journal-title":"JSAT"},{"key":"17_CR19","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1145\/503272.503291","volume-title":"POPL","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Qadeer, S.: Predicate Abstraction for Software Verification. In: POPL, pp. 191\u2013202. ACM Press, New York (2002)"},{"key":"17_CR20","unstructured":"Genaim, S., Giacobazzi, R., Mastroeni, I.: Modeling Secure Information Flow with Boolean Functions. In: IFIP WG 1.7, ACM Workshop on Issues in the Theory of Security, Barcelona, Spain, pp. 55\u201366 (2004)"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"CAV","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of Abstract State Graphs with PVS. In: CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/3-540-40922-X_22","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Gupta","year":"2000","unstructured":"Gupta, A., Yang, Z.-J., Ashar, P., Gupta, A.: SAT-based image computation with application in reachability analysis. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 354\u2013371. Springer, Heidelberg (2000)"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11527695_17","volume-title":"Theory and Applications of Satisfiability Testing","author":"H. Jin","year":"2005","unstructured":"Jin, H., Somenzi, F.: CirCUs: A hybrid satisfiability solver. In: Holger Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 211\u2013223. Springer, Heidelberg (2005)"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/11691372_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Kettle","year":"2006","unstructured":"Kettle, N., King, A., Strzemecki, T.: Widening rOBDDs with prime implicants. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 105\u2013119. Springer, Heidelberg (2006)"},{"key":"17_CR25","volume-title":"The Art of Computer Programming","author":"D.E. Knuth","year":"1997","unstructured":"Knuth, D.E.: The Art of Computer Programming, vol.\u00a03. Addison-Wesley, London (1997)"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-45069-6_15","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 141\u2013153. Springer, Heidelberg (2003)"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/11817963_39","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2006","unstructured":"Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 424\u2013437. Springer, Heidelberg (2006)"},{"key":"17_CR28","first-page":"232","volume-title":"International Conference on Tools with Artificial Intelligence","author":"V.M. Manquinho","year":"1997","unstructured":"Manquinho, V.M., Flores, P.F., Silva, J.P.M., Oliveira, A.L.: Prime Implicant Computation Using Satisfiability Algorithms. In: International Conference on Tools with Artificial Intelligence, pp. 232\u2013239. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 250\u2013264. Springer, Heidelberg (2002)"},{"key":"17_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-14295-6_51","volume-title":"Computer Aided Verification","author":"D. Monniaux","year":"2010","unstructured":"Monniaux, D.: Quantifier elimination by lazy model enumeration. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 585\u2013599. Springer, Heidelberg (2010)"},{"issue":"3","key":"17_CR31","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. Plaisted","year":"1986","unstructured":"Plaisted, D., Greenbaum, S.: A Structure-Preserving Clause Form Translation. Journal of Symbolic Computation\u00a02(3), 293\u2013304 (1986)","journal-title":"Journal of Symbolic Computation"},{"issue":"9","key":"17_CR32","doi-asserted-by":"publisher","first-page":"627","DOI":"10.2307\/2307285","volume":"62","author":"W.V. Quine","year":"1955","unstructured":"Quine, W.V.: A way to simplify truth functions. American Mathematical Monthly\u00a062(9), 627\u2013631 (1955)","journal-title":"American Mathematical Monthly"},{"key":"17_CR33","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/S0167-5060(08)70325-X","volume":"2","author":"R.C. Read","year":"1978","unstructured":"Read, R.C.: Everyone a Winner. Annals of Discrete Mathematics\u00a02, 107\u2013120 (1978)","journal-title":"Annals of Discrete Mathematics"},{"key":"17_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer Aided Verification","author":"H. Sa\u00efdi","year":"1999","unstructured":"Sa\u00efdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 443\u2013454. Springer, Heidelberg (1999)"},{"key":"17_CR35","unstructured":"Samson, E.W., Mills, B.E.: Circuit minimization: Algebra and algorithms for new Boolean canonical expressions. Technical Report TR, pp. 21\u201354. United States Air Force, Cambridge Research Lab (1954)"},{"key":"17_CR36","doi-asserted-by":"crossref","unstructured":"Schlich, B.: Model checking of software for microcontrollers. ACM Trans. Embedded Comput. Syst\u00a09(4), article Number 36 (2010)","DOI":"10.1145\/1721695.1721702"},{"key":"17_CR37","first-page":"10822","volume-title":"DATE","author":"S. Sheng","year":"2003","unstructured":"Sheng, S., Hsiao, M.S.: Efficient Preimage Computation Using A Novel Success-Driven ATPG. In: DATE, pp. 10822\u201310827. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"17_CR38","first-page":"556","volume-title":"FOCS","author":"C. Umans","year":"1998","unstructured":"Umans, C.: The Minimum Equivalent DNF Problem and Shortest Implicants. In: FOCS, pp. 556\u2013563. IEEE Computer Society Press, Los Alamitos (1998)"},{"issue":"2","key":"17_CR39","first-page":"89","volume":"1","author":"S. Weaver","year":"2006","unstructured":"Weaver, S., Franco, J.V., Schlipf, J.S.: Extending Existential Quantification in Conjunctions of BDDs. JSAT\u00a01(2), 89\u2013110 (2006)","journal-title":"JSAT"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22110-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,7]],"date-time":"2023-06-07T19:16:37Z","timestamp":1686165397000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22110-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221095","9783642221101"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22110-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}