{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:24:08Z","timestamp":1721953448252},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656262","type":"print"},{"value":"9783031656279","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"Abstract<\/jats:title>Many program verification tools provide automation via SMT solvers, allowing them to automatically discharge many proofs. However, when a proof fails, it can be hard to understand why it failed or how to fix it. The main feedback the developer receives is simply the verification result (i.e., success or failure), with no visibility into the solver\u2019s internal state. To assist developers using such tools, we introduce ProofPlumber, a novel and extensible proof-action<\/jats:italic> framework for understanding and debugging proof failures. Proof actions act on the developer\u2019s source-level proofs<\/jats:italic> (e.g., assertions and lemmas) to determine why they failed and potentially suggest remedies. We evaluate ProofPlumber by writing a collection of proof actions that capture common proof debugging practices. We produce 17 proof actions, each only 29\u2013177 lines of code.<\/jats:p>","DOI":"10.1007\/978-3-031-65627-9_17","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:01:31Z","timestamp":1721934091000},"page":"348-361","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Framework for\u00a0Debugging Automated Program Verification Proofs via\u00a0Proof Actions"],"prefix":"10.1007","author":[{"given":"Chanhee","family":"Cho","sequence":"first","affiliation":[]},{"given":"Yi","family":"Zhou","sequence":"additional","affiliation":[]},{"given":"Jay","family":"Bosamiya","sequence":"additional","affiliation":[]},{"given":"Bryan","family":"Parno","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"17_CR1","unstructured":"Coq Development Team. The Coq Proof Assistant. https:\/\/coq.inria.fr\/"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"d. Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: International Conference on Automated Deduction (2021)","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"17_CR3","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning (2000)"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. In: International Conference on Automated Deduction (2011)","DOI":"10.1007\/978-3-642-22438-6_11"},{"key":"17_CR5","doi-asserted-by":"publisher","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reasoning 40(1), 35\u201360 (2008). https:\/\/doi.org\/10.1007\/s10817-007-9085-y","DOI":"10.1007\/s10817-007-9085-y"},{"key":"17_CR6","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (2007)"},{"key":"17_CR7","unstructured":"Chlipala, A.: Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2022)"},{"key":"17_CR8","doi-asserted-by":"publisher","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Proceedings of the 2004 International Conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (2004). https:\/\/doi.org\/10.1007\/978-3-540-30569-9_3","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"17_CR9","doi-asserted-by":"publisher","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: advanced specification and verification with JML and ESC\/Java2. In: Proceedings of the 4th International Conference on Formal Methods for Components and Objects (2005). https:\/\/doi.org\/10.1007\/11804192_16","DOI":"10.1007\/11804192_16"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: VCC: contract-based modular verification of concurrent C. In: 31st International Conference on Software Engineering - Companion Volume (2009)","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"17_CR11","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 (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Swamy, N., et al.: 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":"17_CR13","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Wolf, F.A., Arquint, L., Clochard, M., Oortwijn, W., Pereira, J.C., M\u00fcller, P.: Gobra: modular specification and verification of Go programs. In: Computer Aided Verification (CAV) (2021)","DOI":"10.1007\/978-3-030-81685-8_17"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Eilers, M., M\u00fcller, P.: Nagini: a static verifier for Python. In: Computer Aided Verification (2018)","DOI":"10.1007\/978-3-319-96145-3_33"},{"key":"17_CR16","doi-asserted-by":"publisher","unstructured":"Astrauskas, V., M\u00fcller, P., Poli, F., Summers, A.J.: Leveraging Rust types for modular specification and verification. In: Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360573","DOI":"10.1145\/3360573"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Lattuada, A., et al.: Verus: verifying Rust programs using linear ghost types. In: Proceedings of the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) (2023)","DOI":"10.1145\/3586037"},{"key":"17_CR18","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Hoboken (1976)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Tools & Algorithms for the Construction and Analysis of Systems (TACAS) (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: Computer Aided Verification (CAV) (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"17_CR22","doi-asserted-by":"publisher","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla. In: Computer Aided Verification (CAV) (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_1","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: BTOR2, BtorMC and Boolector 3.0. In: Computer Aided Verification (CAV) (2018)","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Matsakis, N.D., Klock, F.S.: The Rust Language. ACM SIGAda Ada Lett. 34(3), 103\u2013104 (2014). https:\/\/doi.org\/10.1145\/2692956.2663188","DOI":"10.1145\/2692956.2663188"},{"key":"17_CR25","unstructured":"Klabnik, S., Nichols, C.: The Rust Programming Language. No Starch Press, San Francisco (2018)"},{"key":"17_CR26","unstructured":"Verification Debugging When Verification Fails. https:\/\/dafny.org\/dafny\/DafnyRef\/DafnyRef#sec-verification-debugging"},{"key":"17_CR27","unstructured":"Sliding Admit Verification Style. https:\/\/github.com\/FStarLang\/FStar\/wiki\/Sliding-admit-verification-style"},{"key":"17_CR28","unstructured":"StackOverflow Question: With Dafny, Verify Function to Count Integer Set Elements less than a Threshold. https:\/\/stackoverflow.com\/questions\/76924944\/with-dafny-verify-function-to-count-integer-set-elements-less-than-a-threshold\/76925258#76925258"},{"key":"17_CR29","unstructured":"StackOverflow Question: Hint on FStar Proof Dead End. https:\/\/stackoverflow.com\/questions\/61938833\/hint-on-fstar-proof-dead-end"},{"key":"17_CR30","unstructured":"Language Server Protocol. https:\/\/microsoft.github.io\/language-server-protocol\/specifications\/lsp\/3.17\/specification\/#textDocument_codeAction"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"van Tonder, R., Le\u00a0Goues, C.: Lightweight multi-language syntax transformation with parser parser combinators. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (2019). https:\/\/doi.org\/10.1145\/3314221.3314589","DOI":"10.1145\/3314221.3314589"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Maletic, J.I., Collard, M.L.: Exploration, analysis, and manipulation of source code using SrcML. In: Proceedings of the 37th International Conference on Software Engineering (2015)","DOI":"10.1109\/ICSE.2015.302"},{"key":"17_CR33","doi-asserted-by":"crossref","unstructured":"Klint, P., van\u00a0der Storm, T., Vinju, J.: RASCAL: a domain specific language for source code analysis and manipulation. In: 2009 Ninth IEEE International Working Conference on Source Code Analysis and Manipulation (2009)","DOI":"10.1109\/SCAM.2009.28"},{"key":"17_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) Conference (2023)"},{"key":"17_CR35","unstructured":"Rust Analyzer. https:\/\/github.com\/rust-lang\/rust-analyzer"},{"key":"17_CR36","doi-asserted-by":"crossref","unstructured":"Mart\u00ednez, G., et al.: $$\\text{Meta-F}^\\star $$: proof automation with SMT, tactics, and metaprograms. In: European Symposium on Programming (2019)","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"Grov, G., Tumas, V.: Tactics for the Dafny program verifier. In: Tools and Algorithms for the Construction and Analysis of Systems (2016)","DOI":"10.1007\/978-3-662-49674-9_3"},{"key":"17_CR38","doi-asserted-by":"crossref","unstructured":"Christakis, M., Leino, K.R.M., M\u00fcller, P., W\u00fcstholz, V.: Integrated environment for diagnosing verification errors. In: Tools and Algorithms for the Construction and Analysis of Systems (2016)","DOI":"10.1007\/978-3-662-49674-9_25"},{"key":"17_CR39","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Fedchin, A., Rakamari\u0107, Z., Rungta, N.: Better counterexamples for Dafny. In: Tools and Algorithms for the Construction and Analysis of Systems (2022)","DOI":"10.1007\/978-3-030-99524-9_23"},{"key":"17_CR40","doi-asserted-by":"crossref","unstructured":"Le\u00a0Goues, C., Leino, K.R.M., Moskal, M.: The Boogie verification debugger. In: Software Engineering and Formal Methods (2011)","DOI":"10.1007\/978-3-642-24690-6_28"},{"key":"17_CR41","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2016). www.SMT-LIB.org"}],"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-65627-9_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:03:52Z","timestamp":1721934232000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65627-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656262","9783031656279"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65627-9_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}