{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T15:20:33Z","timestamp":1782919233765,"version":"3.54.5"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Program verification languages such as Dafny and F\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$ ^\\star $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow\/>\n                            <mml:mo>\u22c6<\/mml:mo>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    often rely heavily on Satisfiability Modulo Theories (SMT) solvers for proof automation. However, SMT-based verification suffers from instability, where semantically irrelevant changes in the source program can cause spurious proof failures.\u00a0While existing mitigation techniques emphasize preemptive measures, we propose\u00a0a complementary approach that focuses on diagnosing and repairing specific instances of instability-induced failures. Our key technique is a novel differential analysis to pinpoint problematic quantified formulas in an unstable query. We implement this technique in Cazamariposas, a tool that automatically identifies such quantified formulas and suggests fixes. We evaluate Cazamariposas on multiple large-scale systems verification projects written in three different program verification languages. Our results demonstrate Cazamariposas \u2019 effectiveness as an instability debugger. In the majority of cases, Cazamariposas successfully isolates the issue to a single problematic quantifier, while providing a stabilizing fix.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_5","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:34Z","timestamp":1753789654000},"page":"75-94","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Cazamariposas: Automated Instability Debugging in\u00a0SMT-Based Program Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7597-1176","authenticated-orcid":false,"given":"Yi","family":"Zhou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-8282-2142","authenticated-orcid":false,"given":"Amar","family":"Shah","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5475-5765","authenticated-orcid":false,"given":"Zhengyao","family":"Lin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9113-1684","authenticated-orcid":false,"given":"Bryan","family":"Parno","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"5_CR1","unstructured":"Amrollahi, D., Preiner, M., Niemetz, A., Reynolds, A., Charikar, M., Tinelli, C., Barrett, C.: Using normalization to improve SMT solver stability (2024), https:\/\/arxiv.org\/abs\/2410.22419"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K., Rungta, N., Tkachuk, O., Varming, C.: Semantic-based automated reasoning for AWS access policies using SMT. In: Formal Methods in Computer Aided Design (FMCAD) (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8602994","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., et\u00a0al.: cvc5: A Versatile and Industrial-Strength SMT Solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Becker, N., M\u00fcller, P., Summers, A.J.: The axiom profiler: Understanding and debugging SMT quantifier instantiations. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2019)","DOI":"10.1007\/978-3-030-17462-0_6"},{"key":"5_CR5","unstructured":"Blanchette, J.C., K\u00fchlwein, D., Geschke, S., Loewe, B., Schlicht, P.: A survey of axiom selection as a machine learning problem. In: Infinity, Computability, and Metamathematics: Festschrift Celebrating the 60th Birthdays of Peter Koepke and Philip Welch. Tributes, College Publications (2014)"},{"key":"5_CR6","unstructured":"B\u00f6hme, S.: Proof reconstruction for Z3 in Isabelle\/HOL. In: International Workshop on Satisfiability Modulo Theories (2009)"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Bordis, T., Leino, K.R.M.: Free facts: An alternative to inefficient axioms in Dafny. In: Formal Methods: 26th International Symposium (FM) (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_8","DOI":"10.1007\/978-3-031-71162-6_8"},{"key":"5_CR8","unstructured":"Cazamariposas. https:\/\/github.com\/secure-foundations\/mariposa, accessed Feb. 2025"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Geldenhuys, J., Heck, M., Hicks, M., Huang, S., Jaloyan, G.A., Joshi, A., Leino, R., Mayer, M., McLaughlin, S., Mritunjai, A., Claudel, C.P., Porncharoenwase, S., Rabe, F., Rapoport, M., Reger, G., Roux, C., Rungta, N., Salkeld, R., Schlaipfer, M., Schoepe, D., Schwartzentruber, J., Tasiran, S., Tomb, A., Torlak, E., Tristan, J., Wagner, L., Whalen, M., Willems, R., Xiang, J., Byun, T.J., Cohen, J., Wang, R., Jang, J., Rath, J., Syeda, H.T., Wagner, D., Yuan, Y.: Formally verified cloud-scale authorization. In: International Conference on Software Engineering (ICSE) (2025), https:\/\/www.amazon.science\/publications\/formally-verified-cloud-scale-authorization","DOI":"10.1109\/ICSE55347.2025.00166"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Cutler, J.W., Disselkoen, C., Eline, A., He, S., Headley, K., Hicks, M., Hietala, K., Ioannidis, E., Kastner, J., Mamat, A., McAdams, D., McCutchen, M., Rungta, N., Torlak, E., Wells, A.M.: Cedar: A new language for expressive, fast, safe, and analyzable authorization. In: Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) (Apr 2024). https:\/\/doi.org\/10.1145\/3649835","DOI":"10.1145\/3649835"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Dodds, M.: Formally Verifying Industry Cryptography. IEEE Security and Privacy Magazine (2022). https:\/\/doi.org\/10.1109\/MSEC.2022.3153035","DOI":"10.1109\/MSEC.2022.3153035"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Ferraiuolo, A., Baumann, A., Hawblitzel, C., Parno, B.: Komodo: Using Verification to Disentangle Secure-Enclave Hardware from Software. In: Proceedings of the ACM Symposium on Operating Systems Principles (SOSP) (2017). https:\/\/doi.org\/10.1145\/3132747.3132782","DOI":"10.1145\/3132747.3132782"},{"key":"5_CR14","unstructured":"Fiala, J.: SmtScope (2025), https:\/\/github.com\/viperproject\/smt-scope, accessed Feb. 2025"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S., Zill, B.: IronFleet: Proving practical distributed systems correct. In: Proceedings of the ACM Symposium on Operating Systems Principles (SOSP) (2015)","DOI":"10.1145\/2815400.2815428"},{"key":"5_CR16","unstructured":"Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad Apps: End-to-end security via automated full-system verification. In: Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) (October 2014)"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: International Conference on Automated Deduction. pp. 299\u2013314. Springer (2011)","DOI":"10.1007\/978-3-642-22438-6_23"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Computer Aided Verification (CAV) (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Lattuada, A., Hance, T., Bosamiya, J., Brun, M., Cho, C., LeBlanc, H., Srinivasan, P., Achermann, R., Chajed, T., Hawblitzel, C., Howell, J., Lorch, J., Padon, O., Parno, B.: Verus: A practical foundation for systems verification. In: Proceedings of the ACM Symposium on Operating Systems Principles (SOSP) (November 2024)","DOI":"10.1145\/3694715.3695952"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Lattuada, A., Hance, T., Cho, C., Brun, M., Subasinghe, I., Zhou, Y., Howell, J., Parno, B., Hawblitzel, C.: Verus: Verifying Rust programs using linear ghost types. In: Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) (December 2023)","DOI":"10.1145\/3586037"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Pit-Claudel, C.: Trigger selection strategies to stabilize program verifiers. In: Chaudhuri, S., Farzan, A. (eds.) Proceedings of the International Conference on Computer Aided Verification (CAV) (2016)","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Moskal, M.: Programming with triggers. In: Proceedings of the Workshop on Satisfiability Modulo Theories (2009)","DOI":"10.1145\/1670412.1670416"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Efficient e-matching for SMT solvers. In: Conference on Automated Deduction (CADE) (2007)","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"5_CR25","unstructured":"Profiling Z3 and solving proof performance issues. https:\/\/fstar-lang.org\/tutorial\/book\/under_the_hood\/uth_smt.html#profiling-z3-and-solving-proof-performance-issues"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Protzenko, J., Parno, B., Fromherz, A., Hawblitzel, C., Polubelova, M., Bhargavan, K., Beurdouche, B., Choi, J., Delignat-Lavaud, A., Fournet, C., Kulatova, N., Ramananandro, T., Rastogi, A., Swamy, N., Wintersteiger, C., Zanella-Beguelin, S.: EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. In: Proceedings of the IEEE Symposium on Security and Privacy (May 2020)","DOI":"10.1109\/SP40000.2020.00114"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Reitz, A., Fromherz, A., Protzenko, J.: StarMalloc: Verifying a modern, hardened memory allocator. Proc. ACM Program. Lang. (Oct 2024). https:\/\/doi.org\/10.1145\/3689773","DOI":"10.1145\/3689773"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Rungta, N.: A billion SMT queries a day (invited paper). In: Shoham, S., Vizel, Y. (eds.) Proceedings of the International Conference on Computer Aided Verification (CAV) (2022)","DOI":"10.1007\/978-3-031-13185-1_1"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) Proc. of the 27th CADE, Natal, Brasil. pp. 495\u2013507. No. 11716 in LNAI, Springer (2019)","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Swamy, N., Hri\u0163cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., Zinzindohoue, J.K., Zanella-B\u00e9guelin, S.: Dependent Types and Multi-Monadic Effects in F*. In: Proceedings of the ACM Symposium on Principles of Programming Languages (POPL) (2016)","DOI":"10.1145\/2837614.2837655"},{"key":"5_CR31","unstructured":"Tomb, A., Tristan, J.B.: Avoiding verification brittleness in Dafny. https:\/\/dafny.org\/blog\/2023\/12\/01\/avoiding-verification-brittleness\/ (2023)"},{"key":"5_CR32","unstructured":"Verification debugging when verification fails. https:\/\/dafny.org\/dafny\/DafnyRef\/DafnyRef#sec-brittle-verification"},{"key":"5_CR33","unstructured":"Zhou, Y., Bosamiya, J., Li, J., Heule, M., Parno, B.: Context pruning for more robust SMT-based program verification. In: Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) Conference (October 2024)"},{"key":"5_CR34","unstructured":"Zhou, Y., Bosamiya, J., Takashima, Y., Li, J., Heule, M., Parno, B.: Mariposa: Measuring SMT instability in automated program verification. In: Proceedings of the Formal Methods in Computer-Aided Design (FMCAD) (October 2023)"},{"key":"5_CR35","doi-asserted-by":"crossref","unstructured":"Zhou, Y., Shah, A., , Lin, Z., Heule, M., Parno, B.: Cazamariposas: Automated Instability Debugging in SMT-based Program Verification (Technical Report). Tech. rep., Carnegie Mellon University (June 2025), doi.org\/10.1184\/R1\/29207189","DOI":"10.1007\/978-3-031-99984-0_5"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:28:15Z","timestamp":1781882895000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","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":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}