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.

References in zbMATH (referenced in 66 articles , 2 standard articles )

Showing results 1 to 20 of 66.
Sorted by year (citations)

1 2 3 4 next

  1. Neider, Daniel; Madhusudan, P.; Saha, Shambwaditya; Garg, Pranav; Park, Daejun: A learning-based approach to synthesizing invariants for incomplete verification engines (2020)
  2. Peña, Ricardo: An assertional proof of red-black trees using Dafny (2020)
  3. Wolter, U. E.; Martini, A. R.; Häusler, E. H.: Indexed and fibred structures for Hoare logic (2020)
  4. Apt, Krzysztof R.; Olderog, Ernst-Rüdiger: Fifty years of Hoare’s logic (2019)
  5. Menghi, Claudio; Spoletini, Paola; Chechik, Marsha; Ghezzi, Carlo: A verification-driven framework for iterative design of controllers (2019)
  6. Milicevic, Aleksandar; Near, Joseph P.; Kang, Eunsuk; Jackson, Daniel: Alloy*: a general-purpose higher-order relational constraint solver (2019)
  7. Bannister, Callum; Höfner, Peter; Klein, Gerwin: Backwards and forwards with separation logic (2018)
  8. Bao, Yuyan; Leavens, Gary T.; Ernst, Gidon: Unifying separation logic and region logic to allow interoperability (2018)
  9. Cao, Qinxiang; Beringer, Lennart; Gruetter, Samuel; Dodds, Josiah; Appel, Andrew W.: VST-Floyd: a separation logic tool to verify correctness of C programs (2018)
  10. Chen, Hao; Wu, Xiongnan; Shao, Zhong; Lockerman, Joshua; Gu, Ronghui: Toward compositional verification of interruptible OS kernels and device drivers (2018)
  11. Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov: Lemma Functions for Frama-C: C Programs as Proofs (2018) arXiv
  12. Lochbihler, Andreas; Schneider, Joshua: Relational parametricity and quotient preservation for modular (co)datatypes (2018)
  13. Melquiond, Guillaume; Rieu-Helft, Raphaël: A Why3 framework for reflection proofs and its application to GMP’s algorithms (2018)
  14. Mendes, Alexandra; Ferreira, João F.: Towards verified handwritten calculational proofs (short paper) (2018)
  15. Müller, Peter (ed.); Schaefer, Ina (ed.): Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018 (2018)
  16. Pedersen, Jan B.; Welch, Peter H.: The symbiosis of concurrency and verification: teaching and case studies (2018)
  17. Rahli, Vincent; Cohen, Liron; Bickford, Mark: A verified theorem prover backend supported by a monotonic library (2018)
  18. Reynolds, Andrew; Viswanathan, Arjun; Barbosa, Haniel; Tinelli, Cesare; Barrett, Clark: Datatypes with shared selectors (2018)
  19. Summers, Alexander J.; Müller, Peter: Automating deductive verification for weak-memory programs (2018)
  20. Zhan, Bohua: Efficient verification of imperative programs using auto2 (2018)

1 2 3 4 next