Automated verification of parallel nested DFS

Publikation: Bidrag til bog/antologi/rapport/proceedingKonferencebidrag i proceedingsForskningpeer review

  • Wytse Oortwijn, Eidgenossische Technische Hochschule Zurich
  • ,
  • Marieke Huisman, University of Twente
  • ,
  • Sebastiaan J.C. Joosten, Dartmouth College
  • ,
  • Jaco van de Pol

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.

OriginalsprogEngelsk
TitelTools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I
RedaktørerArmin Biere, David Parker
Antal sider19
ForlagSpringer
Udgivelsesår2020
Sider247-265
ISBN (trykt)9783030451899
DOI
StatusUdgivet - 2020
Begivenhed26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020 - Dublin, Irland
Varighed: 25 apr. 202030 apr. 2020

Konference

Konference26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020
LandIrland
ByDublin
Periode25/04/202030/04/2020
SerietitelLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind12078 LNCS
ISSN0302-9743

Se relationer på Aarhus Universitet Citationsformater

ID: 186732117