Dafny: An Automatic Program Verifier For Functional Correctness - Leino, Rustan (LPAR-16, Dakar, Senegal, 2010)
Full functional-correctness verification is becoming more automatic Interaction is moving closer to the problem domain A well-designed language and verifier, plus a great SMT solver, go a long way