The OpenMP Analysis Toolkit (OAT) is able to automatically detect data races and deadlocks accurately and efficiently. It includes a novel encoding algorithm specialized for OpenMP programs. In particular, we encode every parallel code region of an OpenMP program into formulae suitable for off-the-shelf SMT-solvers such as Yices. By interpreting the solution reported by Yices, we are able to reproduce a feasible execution trace that reveals the errors. This evidence-based approach not only improves the accuracy of error detection, but is also very useful in debugging programs and fixing problems.
Dr. Liqiang Wang, Computer Science, University of Wyoming, University of Central Florida
Dr. Hongyi Ma, Computer Science, University of Wyoming
Dr. Chunhua Liao, Lawrence Livermore National Laboratory
Dr. Daniel Quinlan, Lawrence Livermore National Laboratory
Dr. Zijiang Yang, Western Michigan University
 Hongyi Ma*, Steve R. Diersen, , Chunhua Liao, Daniel Quinlan, and Zijiang Yang. Symbolic Analysis of Concurrency Errors in OpenMP Programs. In the 42nd International Conference on Parallel Processing (ICPP-2013). October 1-4, 2013, Lyon, France. IEEE Press.
 Hongyi Ma*, , and Krishanthan Krishnamoorthy*. Detecting Thread-Safety Violations in Hybrid OpenMP/MPI Programs. In the 2015 IEEE International Conference on Cluster Computing (CLUSTER 2015), Sept. 2015. Chicago, USA. IEEE Press.