Ştefan Ciobâcă
Alexandru Ioan Cuza University, Iaşi, Romania

Dafny is a verification-oriented programming language, based on deductive verification. It can be used to specify and verify imperative computations. Programming software systems in Dafny increases our level of trust in their correctness, which is desirable for critical systems, such as system software. However, specifying, implementing and verifying software in Dafny can be orders of magnitude more difficult than using a traditional programming language, because of the additional burden of specifying and proving the system. Furthermore, there are comparatively fewer educational resources and less know-how for structuring such verified software. In this talk, I will show how Dafny can be used to specify a recently devised image format based on run-length encoding, and how to implement and verify the corresponding encoding/decoding algorithm. I will go over the various design options for structuring the verification effort. I will explain what is the best structure, which enables a more straight forward verification process.