Multi-core and GPU model checking: Challenges and Outlooks

Model checking is one of the most successful formal techniques for the verification of software and hardware systems. Developed in the beginning of the eighties, nowadays it is used by major companies, like Microsoft, to improve the quality of their products. In my talk I focus on improvements of model checking algorithms by exploiting the recent developments in the processor technology. In particular, the emphasis is on parallel algorithms for shared memory architectures, like multi-core systems and general purpose graphic processing units (GPGPUs). These research directions are quite new - the first papers on multi-core and GPU model checking were published in the last four years. Therefore, there are still many untrodden avenues for cooperation of experts from different computer science communities. For example, one of the main open problems is how to design an efficient (shared memory) parallel algorithm for finding cycles in the state space graph. In the recent years we have been using successfully GPUs for accelerating probabilistic model checking. The implementations in the probabilistic model checker PRISM achieve speedups of more than one order of magnitude compared to their sequential counterparts. Our approach crucially hinges on efficient parallel algorithms for sparse matrix vector multiplication. The above mentioned issues, like cycle detection and multiplication algorithms, are in principle independent on their applications in model checking and as such can be interesting for other computer science areas.