Dafny: An Automatic Program Verifier for Functional Correctness

By K. Rustan, M. Leino. Logic Programming and Automated Reasoning, 2010

1,276 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/6c725d2a7e88515c5f7c877936f90b0184c4fe8f

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

Citations in the corpus

Growing solver-aided languages with rosette (2013, background): “ROSETTE builds on a rich body of prior work on solver-aided languages [5, 23–25, 27, 31, 34, 35] and symbolic evaluation [8, 10, 12, 15, 21, 37, 40].”
Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation (2023, background): “Meanwhile. future work can look into how to integrate EvalPlus with more formal verification ( e.g., Dafny [32]) or validation techniques ( e.g., translation validation [36]) to provide stronger guarantees of the evaluation results when applicable.”
Komodo: Using verification to disentangle secure-enclave hardware from software (2017, methodology): “We specify and verify Komodo using Dafny [51], a general-purpose verification language.”
Dependent types and multi-monadic effects in F* (2016, neutral): “Our online tutorial provides a detailed example illustrating the problem, which is not unique to our system but also affects tools like Dafny (Leino 2010) that adopt a similar, ﬂat memory model.”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, background): “…widely recognized as crucial back-end reasoning engines for a variety of applications, including software and hardware veriﬁcation [19, 52, 60, 68, 82, 86], model checking [41, 42, 98], type checking, static analysis, security [10,62], automated test-case generation [40,135], synthesis [2,65],…”
Why3: Shepherd Your Herd of Provers (2011, background): “This is the case of VCC [12], Spec# [2], Dafny [19], Chalice [20], ESC/Java2 [11], Krakatoa [21], Frama-C [15].”
Deductive Software Verification – The KeY Book (2016, background): “The aforementioned course is currently still taught at Chalmers University3 (with KeY having been replaced by Dafny [Leino, 2010]).”
LightDP: towards automating differential privacy proofs (2016, methodology): “For example, we have formally proved that the transformed program in Figure 1 satisfies a postcondition v ≤ by providing one line of annotation (the grey line in Figure 1) using the Dafny tool (Leino 2010).”