SPADE: verification of multithreaded dynamic and recursive programs
Tayssir Touili ( LIAFA )
- 16:30 16th June 2009 ( week 8, Trinity Term 2009 )Lecture Theatre B
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.
This is a joint work with Gael Patin and Mihaela Sighireanu.