Symbolic Pruning of Concurrent Program Executions

We propose a new algorithm for verifying concurrent programs, which uses concrete executions to partition the program into a set of lean partitions called concurrent trace programs (CTPs), and sym-bolically verifies each CTP using a satisfiability solver. A CTP, derived from a concrete execution trace, implicitly captures all per-mutations of the trace that also respect the control flow of the pro-gram. We show that a CTP, viewed as a coarser equivalence class than the popular (Mazurkiewicz) trace equivalence in partial or-der reduction (POR) literature, leads to more effective pruning of the search space during model checking. While classic POR can prune away redundant interleavings within each trace equivalence class, the pruning in POR is not property driven. We use symbolic methods to achieve property-driven pruning. The effort of explo-ration is distributed between a symbolic component (verification of a particular CTP) and an enumerative component (exploration of the space of CTPs). We show that the proposed method facilitates more powerful pruning of the search space during the enumerative exploration