Automated Verification of Nested DFS

Jan Cornelis van de Pol

doi:10.1007/978-3-319-19458-5_12

Automated Verification of Nested DFS

Jan Cornelis van de Pol

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

610 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 language	Undefined
Title of host publication	Proceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015)
Editors	M. Núñez, M. Güdemann
Place of Publication	Heidelberg
Publisher	Springer
Pages	181-197
Number of pages	17
ISBN (Print)	978-3-319-19457-8
DOIs	https://doi.org/10.1007/978-3-319-19458-5_12
Publication status	Published - Jun 2015
Event	20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015 - Oslo, Norway Duration: 22 Jun 2015 → 23 Jun 2015 Conference number: 20

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	9128
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Workshop

Workshop	20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015
Abbreviated title	FMICS
Country/Territory	Norway
City	Oslo
Period	22/06/15 → 23/06/15

Keywords

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

Access to Document

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

Cite this

@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 ; null ; Conference date: 22-06-2015 Through 23-06-2015",

year = "2015",

month = jun,

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. https://doi.org/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 proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Automated Verification of Nested DFS

AU - van de Pol, Jan Cornelis

N1 - Conference code: 20

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)

A2 - Núñez, M.

A2 - Güdemann, M.

PB - Springer

CY - Heidelberg

Y2 - 22 June 2015 through 23 June 2015

ER -