Verification of C/C++11 Concurrency

Verification of parallel systems is a complex exercise. The large state spaces created due to thread interleavings complicates the verification of such parallel systems. The problem becomes even harder in case of parallel programs executed under relaxed memory models. This work focuses on exploring two approaches – runtime (using DPOR) and thread-modular abstract interpretation to analyse parallel programs under relaxed memory models.

A Sound Reduction of Persistent-Sets for Deadlock Detection in MPI Applications