id: 06068766
dt: a
an: 06068766
au: Rustan, K.; Leino, M.
ti: Developing verified programs with Dafny.
so: Joshi, Rajeev (ed.) et al., Verified software: Theories, tools,
    experiments. 4th international conference, VSTTE 2012, Philadelphia,
    PA, USA, January 28‒29, 2012. Proceedings. Berlin: Springer (ISBN
    978-3-642-27704-7/pbk). Lecture Notes in Computer Science 7152, 82
    (2012).
py: 2012
pu: Berlin: Springer
la: EN
cc: 
ut: 
ci: 
li: doi:10.1007/978-3-642-27705-4_7
ab: Summary: Dafny [2] is a programming language and program verifier. The
    language is type-safe and sequential, and it includes common imperative
    features, dynamic object allocation, and inductive datatypes. It also
    includes specification constructs like pre- and postconditions, which
    let a programmer record the intended behavior of the program along with
    the executable code that is supposed to cause that behavior. Because
    the Dafny verifier runs continuously in the background, the consistency
    of a program and its specifications is always enforced. Dafny has been
    used to verify a number of challenging algorithms, including
    Schorr-Waite graph marking, Floyd’s “tortoise and hare”
    cycle-detection algorithm, and snapshotable trees with iterators. Dafny
    is also being used in teaching and it was a popular choice in the VSTTE
    2012 program verification competition. Its open-source implementation
    has also been used as a foundation for other verification tools. In
    this tutorial, I will give a taste of how to use Dafny in program
    development. This will include an overview of Dafny, basics of writing
    specifications, how to debug verification attempts, how to formulate
    and prove lemmas, and some newer features for staged program
    development.
rv: