PhD Defense: Scalable multi-core model checking

Our modern society relies increasingly on the sound performance of digital systems. Guaranteeing that these systems actually behave correctly according to specification is not a trivial task, yet it is essential for mission-critical systems like auto-pilots, (nuclear) power-plant controllers and your car’s ABS.

The highest degree of certainty about a system’s correctness can be obtained via mathematical proof, a tedious manual process of formally describing and analyzing the system’s behavior. With the invention of "model checking”, the analysis part of this process became automated, by letting a computer exhaustively explore the behavior of the system.

However, the size of the systems that can be "model checked” is severely limited by the available computational resources. Therefore, the goal of the current thesis is to enable the full use of computational power of modern multi-core computers for model checking. The parallel model checking procedures that we present, utilize all available processor cores and obtain a speedup proportional to the number of cores, i.e. they are are “scalable”.

In particular, we adapted concurrent hash tables for multi-core reachability, remaining scalable even with state compression. We devised parallel nested depth-first search algorithms to support model checking of temporal properties in linear time. Finally, to support verification of real-time systems as well, we extended multi-core reachability and temporal-logic checking to the setting of timed automata.

Current trends and future predictions tell us that the available processing cores increase exponentially over time (Moore’s Law). Thus our result stands to gain from this trend. Whether our proposed methods will withstand the ravages of time is to be seen, but so far the speedup of our algorithms has kept up with the 3-fold increase in cores that we have witnessed in the last 4 years during the project.