Teaching Program Verification in Dafny at Amazon (2023)

Introduction We recently made available some teaching material that we have used to teach program verification to scientists and engineers at Amazon. It composed of lecture slides and exercises with solution. If you want to learn about Dafny and program verification, you can jump right in. You will learn how to program in Dafny, how to do use Dafny as a proof assistant, and finally how to verify programs. If instead you are more interested in teaching program verification, you may find the organization of the lectures and the focus on Dafny as a proof assistant surprising, and the following note should provide some context and explanations. Dafny: Program Verifier and Proof Assistant A proof plays two roles. (i) A proof convinces the reader that the statement is correct. (ii) A proof explains why the statement is correct. The first point consists of the administrative (‘bookkeeper’) activities of verifying the correctness of the small reasoning steps and see if they constitut ... Read full article.