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
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: