{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T06:03:09Z","timestamp":1768456989750,"version":"3.49.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995232","type":"print"},{"value":"9783030995249","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a PDR\/IC3 algorithm for finding inductive invariants with quantifier alternations. We tackle scalability issues that arise due to the large search space of quantified invariants by combining a breadth-first search strategy and a new syntactic form for quantifier-free bodies. The breadth-first strategy prevents inductive generalization from getting stuck in regions of the search space that are expensive to search and focuses instead on lemmas that are easy to discover. The new syntactic form is well-suited to lemmas with quantifier alternations by allowing both limited conjunction and disjunction in the quantifier-free body, while carefully controlling the size of the search space. Combining the breadth-first strategy with the new syntactic form results in useful inductive bias by prioritizing lemmas according to: (i) well-defined syntactic metrics for simple quantifier structures and quantifier-free bodies, and (ii) the empirically useful heuristic of preferring lemmas that are fast to discover. On a benchmark suite of primarily distributed protocols and complex Paxos variants, we demonstrate that our algorithm can solve more of the most complicated examples than state-of-the-art techniques.<\/jats:p>","DOI":"10.1007\/978-3-030-99524-9_18","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:14:55Z","timestamp":1648534495000},"page":"338-356","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion"],"prefix":"10.1007","author":[{"given":"Jason R.","family":"Koenig","sequence":"first","affiliation":[]},{"given":"Oded","family":"Padon","sequence":"additional","affiliation":[]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u2019c, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proceedings of the 23rd International Conference on Computer Aided Verification (CAV \u201911). Lecture Notes in Computer Science, vol. 6806, pp. 171\u2013177. Springer (Jul 2011), https:\/\/dl.acm.org\/doi\/10.5555\/2032305.2032319, Snowbird, Utah","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"18_CR2","doi-asserted-by":"publisher","unstructured":"Berkovits, I., Lazic, M., Losa, G., Padon, O., Shoham, S.: Verification of threshold-based distributed algorithms by decomposition to decidable logics. In: Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II. pp. 245\u2013266 (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_15","DOI":"10.1007\/978-3-030-25543-5_15"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 70\u201387. Springer, Berlin Heidelberg, Berlin, Heidelberg (2011), https:\/\/link.springer.com\/chapter\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337\u2013340. TACAS\u201908\/ETAPS\u201908, Springer-Verlag, Berlin, Heidelberg (2008), https:\/\/dl.acm.org\/citation.cfm?id=1792734.1792766","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"18_CR5","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: International Conference on Formal Methods in Computer-Aided Design, FMCAD \u201911, Austin, TX, USA, October 30 - November 02, 2011. pp. 125\u2013134 (2011), https:\/\/dl.acm.org\/citation.cfm?id=2157675"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 259\u2013277. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_14","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"18_CR7","doi-asserted-by":"publisher","unstructured":"Feldman, Y.M., Padon, O., Immerman, N., Sagiv, M., Shoham, S.: Bounded quantifier instantiation for checking inductive invariants. In: Proceedings, Part I, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 10205. pp. 76\u201395. Springer-Verlag, Berlin, Heidelberg (2017). DOI: https:\/\/doi.org\/10.1007\/978-3-662-54577-5_5","DOI":"10.1007\/978-3-662-54577-5_5"},{"key":"18_CR8","doi-asserted-by":"publisher","unstructured":"Feldman, Y.M.Y., Padon, O., Immerman, N., Sagiv, M., Shoham, S.: Bounded quantifier instantiation for checking inductive invariants. Log. Methods Comput. Sci. 15(3) (2019). https:\/\/doi.org\/10.23638\/LMCS-15(3:18)2019","DOI":"10.23638\/LMCS-15(3:18)2019"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Feldman, Y.M.Y., Wilcox, J.R., Shoham, S., Sagiv, M.: Inferring inductive invariants from phase structures. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification. pp. 405\u2013425. Springer International Publishing, Cham (2019), https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-25543-5_23","DOI":"10.1007\/978-3-030-25543-5_23"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE: A Robust Framework for Learning Invariants. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification. pp. 69\u201387. Springer International Publishing, Cham (2014), https:\/\/link.springer.com\/chapter\/10.1007\/978-3-319-08867-9_5","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Goel, A., Sakallah, K.: On symmetry and quantification: A new approach to verify distributed protocols. In: Dutle, A., Moscato, M.M., Titolo, L., Mu\u00f1oz, C.A., Perez, I. (eds.) NASA Formal Methods. pp. 131\u2013150. Springer International Publishing, Cham (2021), https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-76384-8_9","DOI":"10.1007\/978-3-030-76384-8_9"},{"key":"18_CR12","doi-asserted-by":"publisher","unstructured":"Goel, A., Sakallah, K.A.: Towards an automatic proof of Lamport\u2019s Paxos. In: 2021 Formal Methods in Computer Aided Design (FMCAD). pp. 112\u2013122 (2021). https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_20","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_20"},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Lahiri, S.K., Wang, C. (eds.) Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11138, pp. 248\u2013266. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_15","DOI":"10.1007\/978-3-030-01090-4_15"},{"key":"18_CR14","unstructured":"Hance, T., Heule, M., Martins, R., Parno, B.: Finding invariants of distributed systems: It\u2019s a small (enough) world after all. In: Mickens, J., Teixeira, R. (eds.) 18th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2021, April 12-14, 2021. pp. 115\u2013131. USENIX Association (2021), https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance"},{"key":"18_CR15","doi-asserted-by":"publisher","unstructured":"Hassan, Z., Bradley, A.R., Somenzi, F.: Better generalization in IC3. In: 2013 Formal Methods in Computer-Aided Design. pp. 157\u2013164 (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.6679405","DOI":"10.1109\/FMCAD.2013.6679405"},{"key":"18_CR16","doi-asserted-by":"publisher","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7317, pp. 157\u2013171. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"18_CR17","doi-asserted-by":"publisher","unstructured":"Ivrii, A., Gurfinkel, A.: Pushing to the top. In: 2015 Formal Methods in Computer-Aided Design (FMCAD). pp. 65\u201372 (2015). https:\/\/doi.org\/10.1109\/FMCAD.2015.7542254","DOI":"10.1109\/FMCAD.2015.7542254"},{"key":"18_CR18","doi-asserted-by":"publisher","unstructured":"Karbyshev, A., Bj\u00f8rner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. J. ACM 64(1), 7:1\u20137:33 (Mar 2017). https:\/\/doi.org\/10.1145\/3022187","DOI":"10.1145\/3022187"},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"Koenig, J.R., Padon, O., Immerman, N., Aiken, A.: First-order quantified separators. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 703\u2013717. PLDI 2020, Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3385412.3386018","DOI":"10.1145\/3385412.3386018"},{"key":"18_CR20","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: Smt-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0249-4","DOI":"10.1007\/s10703-016-0249-4"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Krishnan, H.G.V., Chen, Y., Shoham, S., Gurfinkel, A.: Global guidance for local generalization in model checking. In: Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. pp. 101\u2013125 (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_7","DOI":"10.1007\/978-3-030-53291-8_7"},{"key":"18_CR22","doi-asserted-by":"publisher","unstructured":"Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16(2), 133\u2013169 (may 1998). https:\/\/doi.org\/10.1145\/279227.279229","DOI":"10.1145\/279227.279229"},{"key":"18_CR23","doi-asserted-by":"publisher","unstructured":"Ma, H., Goel, A., Jeannin, J., Kapritsos, M., Kasikci, B., Sakallah, K.A.: I4: incremental inference of inductive invariants for verification of distributed protocols. In: Brecht, T., Williamson, C. (eds.) Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP 2019, Huntsville, ON, Canada, October 27-30, 2019. pp. 370\u2013384. ACM (2019). https:\/\/doi.org\/10.1145\/3341301.3359651","DOI":"10.1145\/3341301.3359651"},{"key":"18_CR24","doi-asserted-by":"publisher","unstructured":"Marescotti, M., Gurfinkel, A., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Designing parallel PDR. In: Stewart, D., Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017. pp. 156\u2013163. IEEE (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102254","DOI":"10.23919\/FMCAD.2017.8102254"},{"key":"18_CR25","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Lazy annotation revisited. In: Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. pp. 243\u2013259 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_16","DOI":"10.1007\/978-3-319-08867-9_16"},{"key":"18_CR26","unstructured":"mypyvy repository. https:\/\/github.com\/wilcoxjay\/mypyvy"},{"key":"18_CR27","doi-asserted-by":"publisher","unstructured":"Padon, O., Hoenicke, J., Losa, G., Podelski, A., Sagiv, M., Shoham, S.: Reducing liveness to safety in first-order logic. Proc. ACM Program. Lang. 2(POPL) (Dec 2017). https:\/\/doi.org\/10.1145\/3158114","DOI":"10.1145\/3158114"},{"key":"18_CR28","doi-asserted-by":"publisher","unstructured":"Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made EPR: decidable reasoning about distributed protocols. Proceedings of the ACM on Programming Languages 1(OOPSLA), 1\u201331 (Oct 2017). https:\/\/doi.org\/10.1145\/3140568","DOI":"10.1145\/3140568"},{"key":"18_CR29","doi-asserted-by":"publisher","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: Safety verification by interactive generalization. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 614\u2013630. PLDI \u201916, ACM, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2908080.2908118","DOI":"10.1145\/2908080.2908118"},{"key":"18_CR30","doi-asserted-by":"publisher","unstructured":"Taube, M., Losa, G., McMillan, K.L., Padon, O., Sagiv, M., Shoham, S., Wilcox, J.R., Woos, D.: Modularity for decidability of deductive verification with applications to distributed systems. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 662\u2013677. PLDI 2018, Association for Computing Machinery, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3192366.3192414","DOI":"10.1145\/3192366.3192414"},{"key":"18_CR31","doi-asserted-by":"publisher","unstructured":"Zhang, H., Gupta, A., Malik, S.: Syntax-guided synthesis for lemma generation in hardware model checking. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12597, pp. 325\u2013349. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_15","DOI":"10.1007\/978-3-030-67067-2_15"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99524-9_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:23:51Z","timestamp":1648535031000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99524-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995232","9783030995249"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99524-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","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":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","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":"46","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":"4","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":"29% - 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":"10","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)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}