Dafny is a language and auto-active program verifier developed by Microsoft Research.
The Dafny paper is quite an early description I think.
Notes related to Dafny verifier
Papers related to Dafny verifier
- The Boogie verification debugger [legoues:sefm:2011]
- Developing verified programs with Dafny [leino:icse:2013]
- Dafny: An automatic program verifier for functional correctness [leino:lpair:2010]
- Verifying security invariants in ExpressOS [mai:asplos:2013]