KIT | KIT-Bibliothek | Impressum | Datenschutz

Free Facts: An Alternative to Inefficient Axioms in Dafny

Bordis, Tabea ORCID iD icon 1; Leino, K. Rustan M.
1 Karlsruher Institut für Technologie (KIT)

Abstract:

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.

This paper proposes free facts 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.


Verlagsausgabe §
DOI: 10.5445/IR/1000174702
Veröffentlicht am 07.10.2024
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Informationssicherheit und Verlässlichkeit (KASTEL)
Publikationstyp Buchaufsatz
Publikationsjahr 2025
Sprache Englisch
Identifikator ISBN: 978-3-031-71161-9
ISSN: 0302-9743, 1611-3349
KITopen-ID: 1000174702
Erschienen in Formal Methods : 26th International Symposium, FM 2024, Milan, Italy, September 9–13, 2024, Proceedings, Part I. Ed.: A. Platzer, K.Y Rozier, M. Pradella, M. Rossi
Verlag Springer Nature Switzerland
Seiten 151 – 169
Serie Lecture Notes in Computer Science (LNCS) : International Symposium on Formal Methods ; 14933
Vorab online veröffentlicht am 11.09.2024
Nachgewiesen in Scopus
Dimensions
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page