Automated Verification of Parallel Nested DFS

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

doi:10.1007/978-3-030-45190-5_14

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 proceeding › Chapter › Academic › peer-review

5 Citations (Scopus)

137 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 language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	26th 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
Editors	Armin Biere, David Parker
Publisher	Springer
Pages	247-265
ISBN (Electronic)	978-3-030-45190-5
ISBN (Print)	978-3-030-45189-9
DOIs	https://doi.org/10.1007/978-3-030-45190-5_14
Publication status	Published - 2020
Event	26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020 - Dublin, Ireland Duration: 25 Apr 2020 → 30 Apr 2020 Conference number: 26

Publication series

Name	Lecture Notes in Computer Science
Volume	12078

Conference

Conference	26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020
Abbreviated title	TACAS
Country/Territory	Ireland
City	Dublin
Period	25/04/20 → 30/04/20

Access to Document

10.1007/978-3-030-45190-5_14Licence: CC BY

Oortwijn-2020-Automated-verification-of-parallel-Final published version, 382 KBLicence: CC BY

Cite this

Oortwijn, W., Huisman, M., Joosten, S. J. C., & Pol, J. V. D. (2020). Automated Verification of Parallel Nested DFS. In A. Biere, & D. Parker (Eds.), Tools 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, Dublin, Ireland, April 25–30, 2020, Proceedings, Part I (pp. 247-265). (Lecture Notes in Computer Science; Vol. 12078). Springer. https://doi.org/10.1007/978-3-030-45190-5_14

Oortwijn, Wytse ; Huisman, Marieke ; Joosten, Sebastiaan J. C. et al. / Automated Verification of Parallel Nested DFS. Tools 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, Dublin, Ireland, April 25–30, 2020, Proceedings, Part I. editor / Armin Biere ; David Parker. Springer, 2020. pp. 247-265 (Lecture Notes in Computer Science).

@inbook{c24be35b14dc4ec4b80a672a6965a37d,

title = "Automated Verification of Parallel Nested DFS",

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.",

author = "Wytse Oortwijn and Marieke Huisman and Joosten, {Sebastiaan J. C.} and Pol, {Jaco van de}",

year = "2020",

doi = "10.1007/978-3-030-45190-5_14",

language = "English",

isbn = "978-3-030-45189-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "247--265",

editor = "Armin Biere and David Parker",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "Germany",

note = "26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, TACAS ; Conference date: 25-04-2020 Through 30-04-2020",

}

Oortwijn, W, Huisman, M, Joosten, SJC & Pol, JVD 2020, Automated Verification of Parallel Nested DFS. in A Biere & D Parker (eds), Tools 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, Dublin, Ireland, April 25–30, 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12078, Springer, pp. 247-265, 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, Dublin, Ireland, 25/04/20. https://doi.org/10.1007/978-3-030-45190-5_14

Automated Verification of Parallel Nested DFS. / Oortwijn, Wytse; Huisman, Marieke; Joosten, Sebastiaan J. C. et al.
Tools 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, Dublin, Ireland, April 25–30, 2020, Proceedings, Part I. ed. / Armin Biere; David Parker. Springer, 2020. p. 247-265 (Lecture Notes in Computer Science; Vol. 12078).

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

TY - CHAP

T1 - Automated Verification of Parallel Nested DFS

AU - Oortwijn, Wytse

AU - Huisman, Marieke

AU - Joosten, Sebastiaan J. C.

AU - Pol, Jaco van de

N1 - Conference code: 26

PY - 2020

Y1 - 2020

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

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

U2 - 10.1007/978-3-030-45190-5_14

DO - 10.1007/978-3-030-45190-5_14

M3 - Chapter

SN - 978-3-030-45189-9

T3 - Lecture Notes in Computer Science

SP - 247

EP - 265

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Biere, Armin

A2 - Parker, David

PB - Springer

T2 - 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020

Y2 - 25 April 2020 through 30 April 2020

ER -

Oortwijn W, Huisman M, Joosten SJC, Pol JVD. Automated Verification of Parallel Nested DFS. In Biere A, Parker D, editors, Tools 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, Dublin, Ireland, April 25–30, 2020, Proceedings, Part I. Springer. 2020. p. 247-265. (Lecture Notes in Computer Science). doi: 10.1007/978-3-030-45190-5_14

Automated Verification of Parallel Nested DFS

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this