Concurrent Depth-First Search Algorithms
Gavin Lowe ( University of Oxford )
- 11:00 5th March 2014 ( week 7, Hilary Term 2014 )051
We present concurrent algorithms, based on depth-first search, for three problems relevant to model checking: given a state graph, to find its strongly connected components, which states are in loops, and which states are in "lassos". Our algorithms typically exhibit about a four-fold speed-up over the corresponding sequential algorithms on an eight-core machine.