×

Dafny

swMATH ID: 183
Software Authors: Rustan Leino
Description: Dafny is an imperative object-based language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs.The Dafny programming language is designed to support the static verification of programs. It is imperative, sequential, supports generic classes, dynamic allocation, and inductive datatypes, and builds in specification constructs. The specifications include pre- and postconditions, frame specifications (read and write sets), and termination metrics. To further support specifications, the language also offers updatable ghost variables, recursive functions, and types like sets and sequences. Specifications and ghost constructs are used only during verification; the compiler omits them from the executable code.The Dafny verifier is run as part of the compiler. As such, a programmer interacts with it much in the same way as with the static type checker—when the tool produces errors, the programmer responds by changing the program’s type declarations, specifications, and statements.
Homepage: http://research.microsoft.com/en-us/projects/dafny/
Programming Languages: .Net
Operating Systems: Windows
Dependencies: Boogie
Keywords: keywords
Related Software: z3; Boogie; Why3; VeriFast; Coq; VCC; Spec#; Isabelle/HOL; JML; SIMPLIFY; CVC4; Frama-C; KRAKATOA; ESC/Java; WhyML; Viper; PVS; SMT-LIB; Caduceus; VerCors
Referenced in: 69 Publications
all top 5

Referenced by 177 Authors

6 Leino, K. Rustan M.
4 Summers, Alexander J.
3 Filliâtre, Jean-Christophe
3 Müller, Peter
2 Ahrendt, Wolfgang
2 Appel, Andrew W.
2 Barrett, Clark W.
2 Beringer, Lennart
2 Kovács, Laura Ildikó
2 Parkinson, Matthew J.
2 Reynolds, Andrew
2 Rosen, Dan
2 Smallbone, Nicholas
2 Voronkov, Andrei
1 Ahman, Danel
1 Amighi, Afshin
1 Anureev, Igor’ Sergeevich
1 Apt, Krzysztof Rafal
1 Armstrong, Alasdair
1 Banerjee, Anindya
1 Bannister, Callum
1 Bansal, Kshitij
1 Bao, Yuyan
1 Barbosa, Haniel
1 Bickford, Mark
1 Bjørner, Nikolaj S.
1 Blom, Stefan
1 Böhme, Sascha
1 Boström, Pontus
1 Brenas, Jon Haël
1 Cao, Qinxiang
1 Certezeanu, Razvan
1 Chechik, Marsha
1 Chen, Xin
1 Chimento, Jesús Mauricio
1 Chin, Wei-Ngan
1 Christakis, Maria
1 Claessen, Koen
1 Clarke, Edmund Melson jun.
1 Cohen, Liron
1 Cook, William R.
1 Darabi, Saeed
1 Dastani, Mehdi M.
1 Dodds, Josiah
1 Drossopolou, Sophia
1 Drossopoulou, Sophia Chloe
1 Echahed, Rachid
1 Egelund-Muller, Benjamin
1 Eilers, Marco
1 Eisenbach, Susan
1 Ernst, Gidon
1 Feldman, Yotam M. Y.
1 Ferreira, João Filipe
1 Gacek, Andrew
1 Gandhi, Rajeev
1 Garbervetsky, Diego
1 Garg, Pranav
1 Ghezzi, Carlo
1 Gomes, Victor B. F.
1 Gondelman, Léon
1 Gorín, Daniel
1 Grütter, Samuel
1 Gu, Ronghui
1 Haeusler, Edward Hermann
1 Hajdú, Márton
1 He, Guanhua
1 Henzinger, Thomas A.
1 Hobor, Aquinas
1 Höfner, Peter
1 Hozzová, Petra
1 Hriţcu, Cătălin
1 Huisman, Marieke
1 Immerman, Neil
1 Itzhaky, Shachar
1 Jackson, Daniel
1 Johansson, Moa
1 Kang, Eunsuk
1 King, Tim
1 Klein, Gerwin
1 Kobayashi, Naoki
1 Kragl, Bernhard
1 Kröning, Daniel
1 Krosnick, Rebecca
1 Lahiri, Shuvendu Kumar
1 Leavens, Gary T.
1 Leow, Wei Xiang
1 Lochbihler, Andreas
1 Lockerman, Joshua
1 Lucio, Paqui
1 Luo, Chenguang
1 Madhusudan, Parthasarathy
1 Maillard, Kenji
1 Martínez, Guido
1 Martini, A. R.
1 Mar’yasov, Il’ya
1 Meier, Severin
1 Melquiond, Guillaume
1 Mendes, Alexandra
1 Menghi, Claudio
1 Milicevic, Aleksandar
...and 77 more Authors

Referencing Publications by Year