{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T17:11:54Z","timestamp":1743095514012,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031377020"},{"type":"electronic","value":"9783031377037"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,18]],"date-time":"2023-07-18T00:00:00Z","timestamp":1689638400000},"content-version":"vor","delay-in-days":198,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study partial quantifier elimination (PQE) for propositional CNF formulas with existential quantifiers. PQE is a generalization of quantifier elimination where one can limit the set of clauses taken out of the scope of quantifiers to a small subset of clauses. The appeal of PQE is that many verification problems (e.g., equivalence checking and model checking) can be solved in terms of PQE and the latter can be dramatically simpler than full quantifier elimination. We show that PQE can be used for property generation that one can view as a generalization of testing. The objective here is to produce an<jats:italic>unwanted<\/jats:italic>property of a design implementation, thus exposing a bug. We introduce two PQE solvers called<jats:inline-formula><jats:tex-math>$$ EG \\text {-} PQE $$<\/jats:tex-math><\/jats:inline-formula>and<jats:inline-formula><jats:tex-math>$$ EG \\text {-} PQE ^+$$<\/jats:tex-math><\/jats:inline-formula>.<jats:inline-formula><jats:tex-math>$$ EG \\text {-} PQE $$<\/jats:tex-math><\/jats:inline-formula>is a very simple SAT-based algorithm.<jats:inline-formula><jats:tex-math>$$ EG \\text {-} PQE ^+$$<\/jats:tex-math><\/jats:inline-formula>is more sophisticated and robust than<jats:inline-formula><jats:tex-math>$$ EG \\text {-} PQE $$<\/jats:tex-math><\/jats:inline-formula>. We use these PQE solvers to find an unwanted property (namely, an unwanted invariant) of a buggy FIFO buffer. We also apply them to invariant generation for sequential circuits from a HWMCC benchmark set. Finally, we use these solvers to generate properties of a combinational circuit that mimic symbolic simulation.<\/jats:p>","DOI":"10.1007\/978-3-031-37703-7_6","type":"book-chapter","created":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T17:02:15Z","timestamp":1689613335000},"page":"110-131","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Partial Quantifier Elimination and Property Generation"],"prefix":"10.1007","author":[{"given":"Eugene","family":"Goldberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,18]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-13338-6_12","volume-title":"Hardware and Software: Verification and Testing","author":"E Goldberg","year":"2014","unstructured":"Goldberg, E., Manolios, P.: Partial quantifier elimination. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 148\u2013164. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13338-6_12"},{"issue":"3","key":"6_CR2","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symbolic Logic 22(3), 269\u2013285 (1957)","journal-title":"J. Symbolic Logic"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Goldberg, E.: Property checking by logic relaxation, Technical report arXiv:1601.02742 [cs.LO] (2016)","DOI":"10.1109\/FMCAD.2016.7886660"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Goldberg, E.: Partial quantifier elimination and property generation, Technical report arXiv:2303.13811 [cs.LO] (2023)","DOI":"10.1007\/978-3-031-37703-7_6"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Manolios, P.: Software for quantifier elimination in propositional logic. In: ICMS-2014, Seoul, South Korea, 5\u20139 August 2014, pp. 291\u2013294 (2014)","DOI":"10.1007\/978-3-662-44199-2_45"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Goldberg, E.: Equivalence checking by logic relaxation. In: FMCAD-2016, pp. 49\u201356 (2016)","DOI":"10.1109\/FMCAD.2016.7886660"},{"key":"6_CR8","unstructured":"Goldberg, E.: Property checking without inductive invariant generation, Technical report arXiv:1602.05829 [cs.LO] (2016)"},{"key":"6_CR9","unstructured":"B. L. Synthesis and V. Group: ABC: a system for sequential synthesis and verification (2017). www.eecs.berkeley.edu\/~alanmi\/abc"},{"issue":"1\u20132","key":"6_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(98)00017-6","volume":"223","author":"O Kullmann","year":"1999","unstructured":"Kullmann, O.: New methods for 3-SAT decision and worst-case analysis. Theor. Comput. Sci. 223(1\u20132), 1\u201372 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of derivation in the propositional calculus. Zapiski nauchnykh seminarov LOMI, vol. 8, pp. 234\u2013259 (1968). English translation of this volume: Consultants Bureau, N.Y., pp. 115\u2013125 (1970)","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"6_CR12","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":"KL 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. 2404, pp. 250\u2013264. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_19"},{"key":"6_CR13","unstructured":"The source of $${DS}$$-$${PQE}$$. http:\/\/eigold.tripod.com\/software\/ds-pqe.tar.gz"},{"key":"6_CR14","unstructured":"The source of $${EG}$$-$${PQE}$$. http:\/\/eigold.tripod.com\/software\/eg-pqe.1.0.tar.gz"},{"key":"6_CR15","unstructured":"The source of $${EG}$$-$${PQE}^+$$. http:\/\/eigold.tripod.com\/software\/eg-pqe-pl.1.0.tar.gz"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: SAT, Santa Margherita Ligure, Italy, pp. 502\u2013518 (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"6_CR18","unstructured":"An implementation of IC3 by A. Bradley. https:\/\/github.com\/arbrad\/IC3ref"},{"key":"6_CR19","unstructured":"Aniche, M.: Effective Software Testing: A Developer\u2019s Guide. Manning Publications (2022)"},{"key":"6_CR20","unstructured":"HardWare Model Checking Competition (HWMCC-2013) (2013). http:\/\/fmv.jku.at\/hwmcc13\/"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-030-25543-5_6","volume-title":"Computer Aided Verification","author":"MN Rabe","year":"2019","unstructured":"Rabe, M.N.: Incremental determinization for quantifier elimination and functional synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 84\u201394. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_6"},{"key":"6_CR22","unstructured":"CADET. http:\/\/github.com\/MarkusRabe\/cadet"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Bryant, R.: Symbolic simulation\u2013techniques and applications. In: DAC-1990, pp. 517\u2013521 (1990)","DOI":"10.1145\/123186.128296"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35(8), 677\u2013691 (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/3-540-44798-9_24","volume-title":"Correct Hardware Design and Verification Methods","author":"P Chauhan","year":"2001","unstructured":"Chauhan, P., Clarke, E., Jha, S., Kukula, J., Veith, H., Wang, D.: Using combinatorial optimization methods for quantification scheduling. In: Margaria, T., Melham, T. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 293\u2013309. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44798-9_24"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Jin, H., Somenzi, F.: Prime clauses for fast enumeration of satisfying assignments to Boolean circuits. In: DAC 2005, pp. 750\u2013753 (2005)","DOI":"10.1145\/1065579.1065775"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Ganai, M., Gupta, A., Ashar, P.: Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. In: ICCAD-2004, pp. 510\u2013517 (2004)","DOI":"10.1109\/ICCAD.2004.1382631"},{"key":"6_CR28","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). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_30"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-642-22110-1_17","volume-title":"Computer Aided Verification","author":"J Brauer","year":"2011","unstructured":"Brauer, J., King, A., Kriener, J.: Existential quantification as incremental SAT. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 191\u2013207. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_17"},{"key":"6_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-642-40627-0_33","volume-title":"Principles and Practice of Constraint Programming","author":"W Klieber","year":"2013","unstructured":"Klieber, W., Janota, M., Marques-Silva, J., Clarke, E.: Solving QBF with free variables. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 415\u2013431. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40627-0_33"},{"key":"6_CR31","unstructured":"Bjorner, N., Janota, M., Klieber, W.: On conflicts and strategies in QBF. In: LPAR (2015)"},{"key":"6_CR32","unstructured":"Bjorner, N., Janota, M.: Playing with quantified satisfaction. In: LPAR (2015)"},{"key":"6_CR33","unstructured":"Goldberg, E., Manolios, P.: Quantifier elimination by dependency sequents. In: FMCAD-2012, pp. 34\u201344 (2012)"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Manolios, P.: Quantifier elimination via clause redundancy. In: FMCAD 2013, pp. 85\u201392 (2013)","DOI":"10.1109\/FMCAD.2013.6679395"},{"key":"6_CR35","unstructured":"Goldberg, E.: Quantifier elimination with structural learning, Technical report arXiv: 1810.00160 [cs.LO] (2018)"},{"key":"6_CR36","unstructured":"Goldberg, E.: Partial quantifier elimination by certificate clauses, Technical report arXiv:2003.09667 [cs.LO] (2020)"},{"key":"6_CR37","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.: Inductive invariant generation via abductive inference, vol. 48, pp. 443\u2013456, October 2013","DOI":"10.1145\/2544173.2509511"},{"key":"6_CR38","doi-asserted-by":"crossref","unstructured":"Baumgartner, J., Mony, H., Case, M., Sawada, J., Yorav, K.: Scalable conditional equivalence checking: an automated invariant-generation based approach. In: Formal Methods in Computer-Aided Design, pp. 120\u2013127 (2009)","DOI":"10.1109\/FMCAD.2009.5351131"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37703-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,24]],"date-time":"2024-10-24T09:00:39Z","timestamp":1729760439000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37703-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377020","9783031377037"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37703-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"18 July 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}