Analysis of Concurrent Programs

Dealing with complexity of multi-threaded code

Testing parallel or multi-threaded programs is particularly difficult due to the myriad of possibilities in how executions can interleave. Running the same program with the same input argument is likely to yield different interleaving, meaning that not only bugs are hard to find, but also that reproducing them is not easy.

In our research we design clever ways of dealing with concurrent code. This includes using advanced encodings in mathematical formulas, simplifying the analysis by detecting which thread interleavings give the same behaviour, or by applying abstractions that exploit symmetries among the threads.

Read our published work

Sound static deadlock analysis for C/Pthreads by Daniel Kroening, Daniel Poetzl, Peter Schrammel, Björn Wachter

Software Verification for Weak Memory via Program Transformation by Jade Alglave, Daniel Kroening, Vincent Nimal, and Michael Tautschnig

Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs by Vojtech Forejt, Daniel Kroening, Ganesh Narayanaswamy, and Subodh Sharma

Fault Localization in Multi-threaded C Programs Using Bounded Model Checking by Erickson H. da S. Alves, Lucas Cordeiro, Eddie Batista de Lima Filho: