Automated Verification of Nested DFS
| Autor: | van de Pol, Jan Cornelis, Núñez, M., Güdemann, M. |
|---|---|
| Rok vydání: | 2015 |
| Předmět: |
METIS-312650
Model checking Theoretical computer science Programming language Computer science CR-D.2.4 Inductive reasoning automated program verification computer.software_genre Dafny IR-96798 Satisfiability modulo theories Graph (abstract data type) Point (geometry) NDFS Distributed File System Proof obligation EWI-26097 computer |
| Zdroj: | Formal Methods for Industrial Critical Systems ISBN: 9783319194578 FMICS Proceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015), 181-197 STARTPAGE=181;ENDPAGE=197;TITLE=Proceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015) |
| DOI: | 10.1007/978-3-319-19458-5_12 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|