Dafny: An Automatic Program Verifier for Functional Correctness

So, last week the pl reading group chose to read this paper by Rustan Leino. Ignoring the fact that a number of people in our group are interested in this area, Rustan had recently given a presentation on Dafny here (his slides are here) and this was reason we chose this paper.