×

Dafny

swMATH ID: 183
Software Authors: Leino, Rustan
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; Isabelle/HOL; Why3; Coq; VeriFast; VCC; Spec#; CVC4; JML; WhyML; SIMPLIFY; Viper; Frama-C; VerCors; Eiffel; SMT-LIB; GitHub; ESC/Java; Rodin
Cited in: 113 Documents

Standard Articles

2 Publications describing the Software, including 2 Publications in zbMATH Year
Automating induction with an SMT solver. Zbl 1326.68262
Leino, K. Rustan M.
2012
Dafny: an automatic program verifier for functional correctness. Zbl 1253.68095
Leino, K. Rustan M.
2010
all top 5

Cited by 280 Authors

6 Leino, K. Rustan M.
6 Müller, Peter
5 Summers, Alexander J.
3 Appel, Andrew W.
3 Filliâtre, Jean-Christophe
3 Huisman, Marieke
3 Kovács, Laura Ildikó
3 Kuncak, Viktor
3 Schaefer, Ina
2 Ahrendt, Wolfgang
2 Barrett, Clark W.
2 Beringer, Lennart
2 Bian, Jinting
2 de Boer, Frank S.
2 De Gouw, Stijn
2 Drossopoulou, Sophia Chloe
2 Eisenbach, Susan
2 Enea, Constantin
2 Ernst, Gidon
2 Haeusler, Edward Hermann
2 Hiep, Hans-Dieter A.
2 Kobayashi, Naoki
2 Krishna, Siddharth
2 Lucio, Paqui
2 Madhusudan, Parthasarathy
2 Martini, A. R.
2 Montenegro, Manuel
2 Oortwijn, Wytse
2 Parkinson, Matthew J.
2 Potanin, Alex
2 Raya, Rodrigo
2 Reynolds, Andrew
2 Riesco, Adrián
2 Rosen, Dan
2 Rümmer, Philipp
2 Runge, Tobias
2 Schwerhoff, Malte
2 Smallbone, Nicholas
2 Thüm, Thomas
2 Voronkov, Andrei
2 Wies, Thomas
2 Wolter, Uwe E.
2 Zhan, Bohua
1 Abuin, Alex
1 Ahman, Danel
1 Al Wardani, Farah
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 Batista Ribeiro, Leandro
1 Baunach, Marcel
1 Bentkamp, Alexander
1 Bhayat, Ahmed
1 Bickford, Mark
1 Bjørner, Nikolaj S.
1 Blázquez, Jorge
1 Blom, Stefan
1 Böhme, Sascha
1 Bolotov, Alexander
1 Bordis, Tabea
1 Boström, Pontus
1 Brenas, Jon Haël
1 Bugariu, Alexandra
1 Cao, Qinxiang
1 Certezeanu, Razvan
1 Chaudhuri, Kaustuv
1 Chechik, Marsha
1 Chen, Hao
1 Chen, Xin
1 Chen, Zhenbang
1 Chimento, Jesús Mauricio
1 Chin, Wei-Ngan
1 Christakis, Maria
1 Ciobâcă, Ştefan
1 Çirisci, Berk
1 Claessen, Koen
1 Clarke, Edmund Melson jun.
1 Cohen, Liron
1 Cook, William R.
1 Coughlin, Nicholas
1 Cristiá, Maximiliano
1 Dalvandi, Mohammadsadegh
1 Darabi, Saeed
1 Dastani, Mehdi M.
1 De Angelis, Emanuele
1 De Luca, Guido
1 Dodds, Josiah
1 Drossopolou, Sophia
1 Du, Yide
1 Echahed, Rachid
1 Egelund-Muller, Benjamin
1 Eilers, Marco
1 Eisenhofer, Clemens
1 Emmi, Michael
...and 180 more Authors
all top 5

Cited in 11 Serials

9 Formal Aspects of Computing
8 Journal of Automated Reasoning
7 Formal Methods in System Design
6 Journal of Logical and Algebraic Methods in Programming
4 Logical Methods in Computer Science
2 Lecture Notes in Computer Science
1 Journal of Symbolic Computation
1 Mathematical Structures in Computer Science
1 Annals of Mathematics and Artificial Intelligence
1 Joint Bulletin of the Novosibirsk Computing Center (NCC) and A. P. Ershov Institute of Informatics Systems (IIS). Series: Computer Science
1 ACM Transactions on Computational Logic
all top 5

Cited in 7 Fields

111 Computer science (68-XX)
23 Mathematical logic and foundations (03-XX)
3 General and overarching topics; collections (00-XX)
2 Category theory; homological algebra (18-XX)
1 Numerical analysis (65-XX)
1 Operations research, mathematical programming (90-XX)
1 Mathematics education (97-XX)

Citations by Year