Automated Verification of Nested DFS

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    1 Citation (Scopus)
    211 Downloads (Pure)

    Abstract

    In this paper we demonstrate the automated verification of the Nested Depth-First Search (NDFS) algorithm for detecting accepting cycles. The starting point is a recursive formulation of the NDFS algorithm. We use Dafny to annotate the algorithm with invariants and a global specification. The global specification requires that NDFS indeed solves the accepting cycle problem. The invariants are proved automatically by the SMT solver Z3 underlying Dafny. The global specifications, however, need some inductive reasoning on paths in a graph. To prove these properties, some auxiliary lemmas had to be provided. The full specification is contained in this paper. It fits on 4 pages, is verified by Dafny in about 2 minutes, and was developed in a couple of weeks.
    Original languageUndefined
    Title of host publicationProceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015)
    EditorsM. Núñez, M. Güdemann
    Place of PublicationHeidelberg
    PublisherSpringer
    Pages181-197
    Number of pages17
    ISBN (Print)978-3-319-19457-8
    DOIs
    Publication statusPublished - Jun 2015
    Event20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015 - Oslo, Norway
    Duration: 22 Jun 201523 Jun 2015
    Conference number: 20

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume9128
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Workshop

    Workshop20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015
    Abbreviated titleFMICS
    CountryNorway
    CityOslo
    Period22/06/1523/06/15

    Keywords

    • EWI-26097
    • CR-D.2.4
    • automated program verification
    • METIS-312650
    • Dafny
    • NDFS
    • IR-96798

    Cite this

    van de Pol, J. C. (2015). Automated Verification of Nested DFS. In M. Núñez, & M. Güdemann (Eds.), Proceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015) (pp. 181-197). (Lecture Notes in Computer Science; Vol. 9128). Heidelberg: Springer. https://doi.org/10.1007/978-3-319-19458-5_12