Dafny: An Automatic Program Verifier For Functional Correctness
- Rustan Leino
LPAR-16, Dakar, Senegal |
Published by Microsoft Research
- 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