### Abstract

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

State | Published - Jun 2015 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Verlag |

Volume | 9128 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Fingerprint

### Keywords

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

### Cite this

*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

}

*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. DOI: 10.1007/978-3-319-19458-5_12

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

Research output: Scientific - peer-review › Conference 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 -