{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:19:51Z","timestamp":1760015991553,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031711619"},{"type":"electronic","value":"9783031711626"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"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><jats:p>Formal software verification relies on properties of functions and built-in operators. Unless these properties are handled directly by decision procedures, an automated verifier includes them in verification conditions by supplying them as universally quantified axioms or theorems. The use of quantifiers sometimes leads to bad performance, especially if automation causes the quantifiers to be instantiated many times.<\/jats:p><jats:p>This paper proposes <jats:italic>free facts<\/jats:italic> as an alternative to some axioms. A free fact is a pre-instantiated axiom that is generated alongside the formulas in a verification condition that can benefit from the facts. Replacing an axiom with free facts thus reduces the number of quantifiers in verification conditions. Free facts are statically triggered by syntactic occurrences of certain patterns in the proof terms. This is less powerful than the dynamically triggered patterns used during proof construction. However, the paper shows that free facts perform well in practice.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_8","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"151-169","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Free Facts: An Alternative to\u00a0Inefficient Axioms in\u00a0Dafny"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-2886-0862","authenticated-orcid":false,"given":"Tabea","family":"Bordis","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2872-8039","authenticated-orcid":false,"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"8_CR1","unstructured":"Dafny 2024 - POPL 2024. https:\/\/popl24.sigplan.org\/home\/dafny-2024#event-overview. Accessed 15 Mar 2024"},{"key":"8_CR2","unstructured":"Understanding how F* uses Z3 - Proof-Oriented Programming in F* documentation. https:\/\/fstar-lang.org\/tutorial\/book\/under_the_hood\/uth_smt.html. Accessed 01 July 2024"},{"key":"8_CR3","unstructured":"Dafny Documentation (2024). https:\/\/dafny.org\/dafny\/DafnyRef\/DafnyRef.html. Accessed 18 Mar 2024"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-319-21668-3_6","volume-title":"Computer Aided Verification","author":"K Bansal","year":"2015","unstructured":"Bansal, K., Reynolds, A., King, T., Barrett, C., Wies, T.: Deciding local theory extensions via e-matching. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 87\u2013105. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_6"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17","DOI":"10.1007\/11804192_17"},{"key":"8_CR7","unstructured":"Barras, B., et al.: The Coq Proof Assistant Reference Manual\u202f: Version. vol. 6, p. 1 (2006)"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Barrett, C., et al.: Cvc4. In: Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, pp. 171\u2013177. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"8_CR9","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"C Barrett","year":"2018","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-030-17462-0_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Becker","year":"2019","unstructured":"Becker, N., M\u00fcller, P., Summers, A.J.: The axiom profiler: inderstanding and debugging SMT quantifier instantiations. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 99\u2013116. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_6"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Blanc, R., Kuncak, V., Kneuss, E., Suter, P.: An overview of the Leon verification system: verification by translation to recursive functions. In: Proceedings of the 4th Workshop on Scala (SCALA 2013), pp. 1\u201310. Association for Computing Machinery (2013)","DOI":"10.1145\/2489837.2489838"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Bornholt, J., et al.: Using lightweight formal methods to validate a key-value storage node in Amazon S3. In: Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles (SOSP 2021), pp. 836\u2013850. Association for Computing Machinery (2021)","DOI":"10.1145\/3477132.3483540"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Chudnov, A., et al.: Continuous formal verification of Amazon s2n. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 430\u2013446. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_26","DOI":"10.1007\/978-3-319-96142-2_26"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Cohen, E., et al.: VCC: a practical system for verifying concurrent C. In: Theorem Proving in Higher Order Logics: 22nd International Conference, TPHOLs 2009, Munich, 17\u201320 August 2009, pp. 23\u201342. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"8_CR15","unstructured":"Cutler, J.W., Hicks, M., Torlak, E.: Improving the Stability of Type Safety Proofs in Dafny (2024). https:\/\/popl24.sigplan.org\/details\/dafny-2024-papers\/3\/Improving-the-Stability-of-Type-Safety-Proofs-in-Dafny. in\u00a0[1]"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Efficient E-matching for SMT solvers. In: Automated Deduction\u2013CADE-21: 21st International Conference on Automated Deduction Bremen, 17\u201320 July 2007, pp. 183\u2013198. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","DOI":"10.1145\/1066100.1066102"},{"key":"8_CR18","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall (1976)"},{"key":"8_CR19","unstructured":"Furia, C.A., Nordio, Mart\u00edn\u00a0and Polikarpova, N., Tschannen, J.: AutoProof: auto-active functional verification of object-oriented programs. Int. J. Softw. Tools Technol. Transf"},{"key":"8_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3360592","volume":"3","author":"J Hamza","year":"2019","unstructured":"Hamza, J., Voirol, N., Kun\u010dak, V.: System FR: formalized foundations for the stainless verifier. Proc. ACM Program. Lang. 3, 1\u201330 (2019)","journal-title":"Proc. ACM Program. Lang."},{"key":"8_CR21","unstructured":"Hance, T., Lattuada, A., Hawblitzel, C., Howell, J., Johnson, R., Parno, B.: Storage Systems are Distributed Systems (So Verify Them That Way!), pp. 99\u2013115 (2020)"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., et al.: IronFleet: proving practical distributed systems correct. In: Proceedings of the 25th Symposium on Operating Systems Principles (SOSP 2015), pp. 1\u201317. Association for Computing Machinery (2015)","DOI":"10.1145\/2815400.2815428"},{"key":"8_CR23","unstructured":"Ho, S., Pit-Claudel, C.: Incremental Proof Development in Dafny with Module-Based Induction (2024). in\u00a0[1]"},{"key":"8_CR24","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume":"6617","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. NASA Formal Methods 6617, 41\u201355 (2011)","journal-title":"NASA Formal Methods"},{"issue":"3","key":"8_CR25","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015)","journal-title":"Formal Aspects Comput."},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107\u2013115 (2010)","DOI":"10.1145\/1743546.1743574"},{"key":"8_CR27","unstructured":"Leino, K.R.M.: Ecstatic: an object-oriented programming language with an axiomatic semantics. In: The Fourth International Workshop on Foundations of Object-Oriented Languages (1997)"},{"key":"8_CR28","unstructured":"Leino, K.R.M.: Specification and verification of object-oriented software. In: Broy, M., Sitou, W., Hoare, T. (eds.) Engineering Methods and Tools for Software Safety and Security, NATO Science for Peace and Security Series D: Information and Communication Security, vol.\u00a022, pp. 231\u2013266. IOS Press (2009)"},{"key":"8_CR29","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-319-41528-4_20","volume-title":"Computer Aided Verification","author":"KRM Leino","year":"2016","unstructured":"Leino, K.R.M., Pit-Claudel, C.: Trigger selection strategies to stabilize program verifiers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 361\u2013381. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_20"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Liu, J., et al.: P4v: practical verification for programmable data planes. In: Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication ( SIGCOMM 2018), pp. 490\u2013503. Association for Computing Machinery (2018)","DOI":"10.1145\/3230543.3230582"},{"key":"8_CR32","unstructured":"McLaughlin, S., Jaloyan, G.A., Xiang, T., Rabe, F.: Enhancing Proof Stability (2024). https:\/\/popl24.sigplan.org\/details\/dafny-2024-papers\/14\/Enhancing-Proof-Stability, in\u00a0[1]"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"8_CR34","unstructured":"Mugnier, E., McLaughlin, S., Tomb, A.: Portfolio Solving for Dafny (2024). https:\/\/popl24.sigplan.org\/details\/dafny-2024-papers\/8\/Portfolio-Solving-for-Dafny, in\u00a0[1]"},{"key":"8_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Nelson, L., Bornholt, J., Gu, R., Baumann, A., Torlak, E., Wang, X.: Scaling symbolic evaluation for automated verification of systems sode with serval. In: Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP 2019), pp. 225\u2013242. Association for Computing Machinery (2019)","DOI":"10.1145\/3341301.3359641"},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"Protzenko, J., et al.: EverCrypt: a fast, verified, cross-platform cryptographic provider. In: 2020 IEEE Symposium on Security and Privacy (SP), pp. 983\u20131002 (2020)","DOI":"10.1109\/SP40000.2020.00114"},{"key":"8_CR38","unstructured":"Srinivasan, P., Padon, O., Howell, J., Lattuada, A.: Domesticating Automation (2024). https:\/\/popl24.sigplan.org\/details\/dafny-2024-papers\/2\/Domesticating-Automation. in\u00a0[1]"},{"key":"8_CR39","doi-asserted-by":"crossref","unstructured":"Swamy, N., et al.: Dependent types and multi-monadic effects in F*. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), pp. 256\u2013270. Association for Computing Machinery (2016)","DOI":"10.1145\/2837614.2837655"},{"key":"8_CR40","doi-asserted-by":"crossref","unstructured":"Vazou, N., et al.: Refinement reflection: complete verification with SMT. Proc. ACM Program. Lang. 2(POPL), 1\u201331 (2017)","DOI":"10.1145\/3158141"},{"key":"8_CR41","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 23rd Conference on Formal Methods in Computer-Aided Design (FMCAD 2023), pp. 178\u2013188 (2023)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:03:47Z","timestamp":1725933827000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}