33
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      A Tutorial on Using Dafny to Construct Verified Software

      Preprint

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          This paper is a tutorial for newcomers to the field of automated verification tools, though we assume the reader to be relatively familiar with Hoare-style verification. In this paper, besides introducing the most basic features of the language and verifier Dafny, we place special emphasis on how to use Dafny as an assistant in the development of verified programs. Our main aim is to encourage the software engineering community to make the move towards using formal verification tools.

          Related collections

          Most cited references21

          • Record: found
          • Abstract: not found
          • Conference Proceedings: not found

          seL4

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Specification and verification

              Bookmark
              • Record: found
              • Abstract: not found
              • Book: not found

              Programming Languages and Systems

                Bookmark

                Author and article information

                Journal
                2017-01-16
                Article
                10.4204/EPTCS.237.1
                1701.04481
                3306f00b-71da-44d1-93f3-92f5b33f2386

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                EPTCS 237, 2017, pp. 1-19
                In Proceedings PROLE 2016, arXiv:1701.03069
                cs.SE cs.LO cs.PL
                EPTCS

                Software engineering,Theoretical computer science,Programming languages
                Software engineering, Theoretical computer science, Programming languages

                Comments

                Comment on this article

                scite_
                0
                0
                0
                0
                Smart Citations
                0
                0
                0
                0
                Citing PublicationsSupportingMentioningContrasting
                View Citations

                See how this article has been cited at scite.ai

                scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.

                Similar content342

                Most referenced authors87