Exploring the program verifier Dafny that can compile to other languages
A case-study of Dafny, a formal verification tool
J.G. Koelewijn (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Benedikt Ahrens – Mentor (TU Delft - Programming Languages)
M. Izadi – Graduation committee member (TU Delft - Software Engineering)
K.F. Wullaert – Mentor (TU Delft - Programming Languages)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Formal verification is a stricter way of ensuring correctness of a program, but sitting down
and writing the proof yourself is often time-consuming. SMT solvers try to automate parts of this
process. This paper aims to explore Dafny, a programming language and verifier that uses an SMT
solver underneath to do this verification. This paper will go over its logical foundations, and how
it can be used to verify an in-place selection sort algorithm as well as a key-value store. It will
also explore a feature of Dafny that allows the user to compile to other languages, and will discuss
its usefulness in the industry. Verifying the sorting algorithm was very straightforward while the
key-value store posed some problems. However, Dafny itself seems to be very straightforward
to program in. Its ability to compile to other languages leaves a lot to be desired. While the
compiled code is fully functional, the code is barely readable and less than ideal to work with. A
further study discussing Dafny’s ease of use compared to other tools could be conducted to see if
the lacking compiler could outweigh having a native verifier specifically designed for a high-level
programming language.