Smarter bug checking by containing the state space explosion

Eindhoven University of Technology PhD candidate Thomas Neele has developed three techniques for smarter and faster bug checking, based on the model checking method. In his work, carried out in collaboration with ASML, he addresses the infamous state space explosion problem by reducing the number of software states that need to be checked. On 16 September, he’ll defend his thesis, called “Reductions for parity games and model checking.”

Model checking is one of the most rigorous techniques to check software. It looks at all possible things a software system can do, and the states it can be in, to check if it works as required. The challenge is that software often consists of many parts that work in parallel. That can cause an explosion in the number of states that need to be investigated, making model checking costly and perhaps even unmanageable.

The three new reduction techniques Neele developed in his PhD project have one thing in common: they take the requirement of the states in mind. This extra piece of information means it’s easier to see which states don’t need checking. To be able to look at the system’s behavior and requirement at the same time, Neele first developed a new, structured way to show the behavior-requirement combination.