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
StatePublished - Jun 2015
Event20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015 - Oslo, Norway

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

Fingerprint

Specifications
Surface mount technology

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). ed. / M. Núñez; M. Güdemann. Heidelberg : Springer, 2015. p. 181-197 (Lecture Notes in Computer Science; Vol. 9128).

Research output: Scientific - peer-reviewConference contribution

@inbook{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",
isbn = "978-3-319-19457-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "181--197",
editor = "M. Núñez and M. Gü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-23 June. 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: Scientific - peer-reviewConference contribution

TY - CHAP

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

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