Automated Verification of Parallel Nested DFS

Wytse Oortwijn, Marieke Huisman, Sebastiaan J. C. Joosten, Jaco van de Pol

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

1 Citation (Scopus)
7 Downloads (Pure)

Abstract

Model checking algorithms are typically complex graph algorithms, whose correctness is crucial for the usability of a model checker. However, establishing the correctness of such algorithms can be challenging and is often done manually. Mechanising the verification process is crucially important, because model checking algorithms are often parallelised for efficiency reasons, which makes them even more error-prone. This paper shows how the VerCors concurrency verifier is used to mechanically verify the parallel nested depth-first search (NDFS) graph algorithm of Laarman et al. [25]. We also demonstrate how having a mechanised proof supports the easy verification of various optimisations of parallel NDFS. As far as we are aware, this is the first automated deductive verification of a multi-core model checking algorithm.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings, Part I
EditorsArmin Biere, David Parker
PublisherSpringer
Pages247-265
ISBN (Electronic)978-3-030-45190-5
ISBN (Print)978-3-030-45189-9
DOIs
Publication statusPublished - 2020
Event26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020 - Dublin, Ireland
Duration: 25 Apr 202030 Apr 2020
Conference number: 26

Publication series

NameLecture Notes in Computer Science
Volume12078

Conference

Conference26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020
Abbreviated titleTACAS
CountryIreland
CityDublin
Period25/04/2030/04/20

Fingerprint Dive into the research topics of 'Automated Verification of Parallel Nested DFS'. Together they form a unique fingerprint.

Cite this