Sciweavers

Share
SIGSOFT
2009
ACM

Symbolic pruning of concurrent program executions

10 years 6 months ago
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 symbolically verifies each CTP using a satisfiability solver. A CTP, derived from a concrete execution trace, implicitly captures all permutations of the trace that also respect the control flow of the program. We show that a CTP, viewed as a coarser equivalence class than the popular (Mazurkiewicz) trace equivalence in partial order 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 exploration is distributed between a symbolic component (verification of a particular CTP) and an enumerative component (exploration of the space of CTPs). ...
Chao Wang, Swarat Chaudhuri, Aarti Gupta, Yu Yang
Added 19 Nov 2009
Updated 19 Nov 2009
Type Conference
Year 2009
Where SIGSOFT
Authors Chao Wang, Swarat Chaudhuri, Aarti Gupta, Yu Yang
Comments (0)
books