@InProceedings{10.1007/978-3-030-45190-5_14,
author="Oortwijn, Wytse
and Huisman, Marieke
and Joosten, Sebastiaan J. C.
and van de Pol, Jaco",
editor="Biere, Armin
and Parker, David",
title="Automated Verification of Parallel Nested DFS",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="247--265",
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.",
isbn="978-3-030-45190-5"
}

{"_id":"HXsSsKgy3AgARowXA","bibbaseid":"oortwijn-huisman-joosten-vandepol-automatedverificationofparallelnesteddfs-2020","authorIDs":[],"author_short":["Oortwijn, W.","Huisman, M.","Joosten, S. J. C.","van de Pol, J."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Oortwijn"],"firstnames":["Wytse"],"suffixes":[]},{"propositions":[],"lastnames":["Huisman"],"firstnames":["Marieke"],"suffixes":[]},{"propositions":[],"lastnames":["Joosten"],"firstnames":["Sebastiaan","J.","C."],"suffixes":[]},{"propositions":["van","de"],"lastnames":["Pol"],"firstnames":["Jaco"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Biere"],"firstnames":["Armin"],"suffixes":[]},{"propositions":[],"lastnames":["Parker"],"firstnames":["David"],"suffixes":[]}],"title":"Automated Verification of Parallel Nested DFS","booktitle":"Tools and Algorithms for the Construction and Analysis of Systems","year":"2020","publisher":"Springer International Publishing","address":"Cham","pages":"247–265","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.","isbn":"978-3-030-45190-5","bibtex":"@InProceedings{10.1007/978-3-030-45190-5_14,\nauthor=\"Oortwijn, Wytse\nand Huisman, Marieke\nand Joosten, Sebastiaan J. C.\nand van de Pol, Jaco\",\neditor=\"Biere, Armin\nand Parker, David\",\ntitle=\"Automated Verification of Parallel Nested DFS\",\nbooktitle=\"Tools and Algorithms for the Construction and Analysis of Systems\",\nyear=\"2020\",\npublisher=\"Springer International Publishing\",\naddress=\"Cham\",\npages=\"247--265\",\nabstract=\"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.\",\nisbn=\"978-3-030-45190-5\"\n}\n\n\n\n","author_short":["Oortwijn, W.","Huisman, M.","Joosten, S. J. C.","van de Pol, J."],"editor_short":["Biere, A.","Parker, D."],"key":"10.1007/978-3-030-45190-5_14","id":"10.1007/978-3-030-45190-5_14","bibbaseid":"oortwijn-huisman-joosten-vandepol-automatedverificationofparallelnesteddfs-2020","role":"author","urls":{},"metadata":{"authorlinks":{}},"downloads":0},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","creationDate":"2020-03-11T13:41:07.969Z","downloads":0,"keywords":[],"search_terms":["automated","verification","parallel","nested","dfs","oortwijn","huisman","joosten","van de pol"],"title":"Automated Verification of Parallel Nested DFS","year":2020,"dataSources":["2tJugFYAignELAmZo","zT4KxAXTKvhK2Hrr4","cCvCnPTRQYq3qPe9y"]}