Automated Verification of Parallel Nested DFS
Wytse Oortwijn
1 , Marieke Huisman
2 ,
Sebastiaan J. C. Joosten
3 , and Jaco van de Pol
2,4
1 Department of Computer Science, ETH Zurich,
Zurich, Switzerland
wytse.oortwijn@inf.ethz.ch
2 Formal Methods and Tools, University of Twente, Enschede, The Netherlands
m.huisman@utwente.nl
3 Dartmouth College, Hanover NH, USA
sebastiaan.joosten@dartmouth.edu
4 Department of Computer Science, Aarhus University, Aarhus, Denmark
jaco@cs.au.dk
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.
1 Introduction
Model checking is an automated procedure for verifying behavioural properties
of reactive systems. To avoid a false sense of safety, it is essential that model
checkers are themselves correct. However, model checkers use ever more ingenious algorithms [12] and even parallel implementations [2] to be able to combat
the large state spaces of critical industrial systems, which makes it increasingly
difficult to guarantee their correctness.
This paper focusses on the mechanical verification of a multi-core model
checking algorithm for detecting accepting cycles in automata, called nested
depth-first search (NDFS). This algorithm solves the model checking problem
for Linear-time Temporal Logic (LTL), a widely used logic for specifying reactive
systems. Multi-core NDFS is developed by Laarman et al. in 2011 [25] and is
currently deployed in the high-performance model checker LTSmin [23].
The mechanical verification of parallel NDFS is carried out in VerCors [6], a
verifier based on concurrent separation logic that targets real-world concurrent
This research has been performed while working at the University of Twente.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 247–265, 2020.
https://doi.org/10.1007/978-3-030-45190-5 14
TACAS
Evaluation
Artifact
2020
Accepted
Wytse Oortwijn
1 , Marieke Huisman
2 ,
Sebastiaan J. C. Joosten
3 , and Jaco van de Pol
2,4
1 Department of Computer Science, ETH Zurich,
Zurich, Switzerland
wytse.oortwijn@inf.ethz.ch
2 Formal Methods and Tools, University of Twente, Enschede, The Netherlands
m.huisman@utwente.nl
3 Dartmouth College, Hanover NH, USA
sebastiaan.joosten@dartmouth.edu
4 Department of Computer Science, Aarhus University, Aarhus, Denmark
jaco@cs.au.dk
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.
1 Introduction
Model checking is an automated procedure for verifying behavioural properties
of reactive systems. To avoid a false sense of safety, it is essential that model
checkers are themselves correct. However, model checkers use ever more ingenious algorithms [12] and even parallel implementations [2] to be able to combat
the large state spaces of critical industrial systems, which makes it increasingly
difficult to guarantee their correctness.
This paper focusses on the mechanical verification of a multi-core model
checking algorithm for detecting accepting cycles in automata, called nested
depth-first search (NDFS). This algorithm solves the model checking problem
for Linear-time Temporal Logic (LTL), a widely used logic for specifying reactive
systems. Multi-core NDFS is developed by Laarman et al. in 2011 [25] and is
currently deployed in the high-performance model checker LTSmin [23].
The mechanical verification of parallel NDFS is carried out in VerCors [6], a
verifier based on concurrent separation logic that targets real-world concurrent
This research has been performed while working at the University of Twente.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 247–265, 2020.
https://doi.org/10.1007/978-3-030-45190-5 14
TACAS
Evaluation
Artifact
2020
Accepted