Dafny

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 27 articles , 2 standard articles )

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

1 2 next

  1. Armstrong, Alasdair; Gomes, Victor B.F.; Struth, Georg: Building program construction and verification tools from algebraic principles (2016)
  2. Filli^atre, Jean-Christophe; Gondelman, Léon; Paskevich, Andrei: The spirit of ghost code (2016)
  3. Tan, Jiaqi; Tay, Hui Jun; Gandhi, Rajeev; Narasimhan, Priya: AUSPICE-R: automatic safety-property proofs for realistic features in machine code (2016)
  4. Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
  5. Ahrendt, Wolfgang; Kovács, Laura; Robillard, Simon: Reasoning about loops using Vampire in KeY (2015)
  6. Dalvandi, Mohammadsadegh; Butler, Michael; Rezazadeh, Abdolbaghi: From Event-B models to Dafny code contracts (2015)
  7. Leino, K.Rustan M.; Lucio, Paqui: An assertional proof of the stability and correctness of Natural Mergesort (2015)
  8. Rosén, Dan; Smallbone, Nicholas: TIP: tools for inductive provers (2015)
  9. David R. Cok: OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse (2014) arXiv
  10. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  11. Leino, K.Rustan M.: Automating theorem proving with SMT (2013)
  12. Qin, Shengchao; He, Guanhua; Luo, Chenguang; Chin, Wei-Ngan; Chen, Xin: Loop invariant synthesis in a combined abstract domain (2013)
  13. Reddy, Uday S.: Automata-theoretic semantics of idealized Algol with passive expressions (2013)
  14. Anureev, I.S.; Mar’yasov, Il’ya; Nepomniashchiĭ, V.A.: Two-level mixed verification method of C-light programs in terms of safety logic (2012)
  15. Bjørner, Nikolaj: Taking satisfiability to the next level with Z3 (abstract) (2012)
  16. Christakis, Maria; Müller, Peter; Wüstholz, Valentin: Collaborative verification and testing with explicit assumptions (2012)
  17. Leino, K.Rustan M.: Automating induction with an SMT solver (2012)
  18. Leino, K.Rustan M.; Yessenov, Kuat: Stepwise refinement of heap-manipulating code in Chalice (2012)
  19. Nedunuri, Srinivas; Smith, Douglas R.; Cook, William R.: Theory and techniques for synthesizing efficient breadth-first search algorithms (2012)
  20. Parkinson, Matthew J.; Summers, Alexander J.: The relationship between separation logic and implicit dynamic frames (2012)

1 2 next