I. Introduction and Motivation
With the advancements in multi-core hardware technology and distributed systems, parallel programming applications have become an essential requisite to manipulate large data and to facilitate multi-tasking of jobs. Ensuring the correctness of these software is a challenging task due to nondeterminism which is a common spirit amongst the applications of multiple parallel programming paradigms. On one extreme, we have formal verification techniques like theorem proving and model-checking which are not scalable, and on the other extreme, we have testing techniques that can not be used to guarantee a lack of errors. Dynamic verification is a lucrative trade-off between testing and formal verification in terms of coverage and scalability. However, we observe the following shortcomings: