Thread alternation aggravates the difficulty of concurrent program verification since the number of traces to be explored grows rapidly as the scale of a concurrent program increases. \textit{Partial-Order Reduction} (POR) techniques alleviate the trace-space explosion problem by partitioning the traces into different equivalent classes. However, due to the coarse dependency approximation of transitions, there are still a large number of redundant traces explored throughout the verification. In this paper, a symbolic approach, namely \textit{Prioritized Constraint-Aided Dynamic Partial-Order Reduction} (PC-DPOR), is proposed to reduce the redundant traces. Specifically, a constrained dependency graph is presented to refine dependencies between transitions, and the exploration of isolated transitions in the graph is prioritized to reduce redundant equivalent traces. Further, we utilize the generated constraints to dynamically detect whether the enabled transitions at the given reachable states are dependent, and thereby to overcome the inherent imprecision of the traditional dependence over-approximation. We have implemented the proposed approach as an extension of CPAchecker by utilizing BDDs as the representation of state sets. Experimental results show that our approach can effectively reduce the time and memory consumption for verifying concurrent programs. In particular, the number of explored states is reduced to 8.62% on average.

Jie Su

Xidian University

China

Cong Tian

Xidian University

Zuchao Yang

Xidian University

Jiyu Yang

Xidian University

Bin Yu

Xidian University

Zhenhua Duan

Xidian University

China