Verification of C11 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. Under this project we are investigating two directions:
- A runtime analysis that uses dynamic partial order reduction (DPOR) to verify other multi-copy atomic (oMCA) behaviors of C++11 programs
- A static analysis of Release-Acquire memory fragment of C11 concurrency by exploiting thread-modular abstract interpretation technique.
These projects is funded by the DST Early Career Research grant.