• DocumentCode
    635290
  • Title

    Developing verified programs with Dafny

  • Author

    Leino, K. Rustan M.

  • Author_Institution
    Microsoft Res., Redmond, WA, USA
  • fYear
    2013
  • fDate
    18-26 May 2013
  • Firstpage
    1488
  • Lastpage
    1490
  • Abstract
    Dafny is a programming language and program verifier. The language includes specification constructs and the verifier checks that the program lives up to its specifications. These tutorial notes give some Dafny programs used as examples in the tutorial.
  • Keywords
    program verification; specification languages; Dafny programs; program verifier; programming language; specification langauge; Arrays; Cognition; Computer languages; Educational institutions; Reactive power; Security; Tutorials;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Software Engineering (ICSE), 2013 35th International Conference on
  • Conference_Location
    San Francisco, CA
  • Print_ISBN
    978-1-4673-3073-2
  • Type

    conf

  • DOI
    10.1109/ICSE.2013.6606754
  • Filename
    6606754