# A Tutorial on Using Dafny to Construct Verified Software

## TL;DR

This tutorial introduces Dafny, a formal verification tool, emphasizing its use in developing verified software and encouraging software engineers to adopt formal methods.

## Contribution

It provides a comprehensive introduction to Dafny's features and demonstrates how to leverage it as an assistant in verified software development.

## Key findings

- Dafny simplifies the process of writing verified programs.
- The tutorial encourages adoption of formal verification in software engineering.
- Dafny's features support effective verification of program correctness.

## Abstract

This paper is a tutorial for newcomers to the field of automated verification tools, though we assume the reader to be relatively familiar with Hoare-style verification. In this paper, besides introducing the most basic features of the language and verifier Dafny, we place special emphasis on how to use Dafny as an assistant in the development of verified programs. Our main aim is to encourage the software engineering community to make the move towards using formal verification tools.