Skip to main content

SPADE: verification of multithreaded dynamic and recursive programs

Tayssir Touili ( LIAFA )
We consider the problem of model-checking multithreaded programs with recursive procedure calls, result passing between recursive procedures, dynamic creation of parallel processes, and synchronisation between parallel threads. To represent such programs accurately, we define a model based on rewrite systems called SPAD. We consider the reachability problem of this model, which is undecidable. We reduce this problem to the computation of abstractions of the sets of execution paths of the program, and we propose a generic technique that can compute different abstractions (of different precisions and different costs) of these sets. We implemented our techniques in a tool called SPADE, and we applied this tool to different case studies. Our results are encouraging. In particular, we were able to automatically find two bugs in two versions of a Windows NT Bluetooth driver.

This is a joint work with Gael Patin and Mihaela Sighireanu.

Share this: