Automated Verification of Nested DFS

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
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
StatePublished - 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. DOI: 10.1007/978-3-319-19458-5_12
van de Pol, Jan Cornelis. / Automated Verification of Nested DFS. Proceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015). editor / M. Núñez ; M. Güdemann. Heidelberg : Springer, 2015. pp. 181-197 (Lecture Notes in Computer Science).
@inproceedings{be6f3d05aeb44d3eacbad0bbfb323b82,
title = "Automated Verification of Nested DFS",
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.",
keywords = "EWI-26097, CR-D.2.4, automated program verification, METIS-312650, Dafny, NDFS, IR-96798",
author = "{van de Pol}, {Jan Cornelis}",
note = "eemcs-eprint-26097",
year = "2015",
month = "6",
doi = "10.1007/978-3-319-19458-5_12",
language = "Undefined",
isbn = "978-3-319-19457-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "181--197",
editor = "M. N{\'u}{\~n}ez and M. G{\"u}demann",
booktitle = "Proceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015)",

}

van de Pol, JC 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). Lecture Notes in Computer Science, vol. 9128, Springer, Heidelberg, pp. 181-197, 20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015, Oslo, Norway, 22/06/15. DOI: 10.1007/978-3-319-19458-5_12

Automated Verification of Nested DFS. / van de Pol, Jan Cornelis.

Proceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015). ed. / M. Núñez; M. Güdemann. Heidelberg : Springer, 2015. p. 181-197 (Lecture Notes in Computer Science; Vol. 9128).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Automated Verification of Nested DFS

AU - van de Pol,Jan Cornelis

N1 - eemcs-eprint-26097

PY - 2015/6

Y1 - 2015/6

N2 - 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.

AB - 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.

KW - EWI-26097

KW - CR-D.2.4

KW - automated program verification

KW - METIS-312650

KW - Dafny

KW - NDFS

KW - IR-96798

U2 - 10.1007/978-3-319-19458-5_12

DO - 10.1007/978-3-319-19458-5_12

M3 - Conference contribution

SN - 978-3-319-19457-8

T3 - Lecture Notes in Computer Science

SP - 181

EP - 197

BT - Proceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015)

PB - Springer

CY - Heidelberg

ER -

van de Pol JC. Automated Verification of Nested DFS. In Núñez M, Güdemann M, editors, Proceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015). Heidelberg: Springer. 2015. p. 181-197. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-19458-5_12