Partial Order Reduction in Symbolic Execution for Object-Oriented Languages

Abstract

The path explosion problem is a significant issue for verification tools that use symbolic execution. Monotonic partial order reduction introduces a sound and complete method of pruning paths irrelevant to the verification process. It does this by finding dependencies within transitions, chaining them, and determining if a computation can be considered quasi-monotonic; if not, the path can be pruned. The algorithm does not clarify possible dependencies between symbolic or concrete references to objects and arrays that must be considered when pruning paths in a concurrent object-oriented language. The contributions made by this research are the extension of the original monotonic partial order reduction method, as well as a performance study of the algorithm when implemented in a symbolic execution verification tool. After a comprehensive, in-depth look at the monotonic partial order reduction algorithm, it was implemented in a verification tool for an intermediate object-oriented language called OOX. When testing the verification tool using many benchmark programs, it is shown that the algorithm remained sound in the pruning of paths and is complete over most scenarios (does not allow for pruning paths using assumptions made over symbolic references). The testing also showed that the algorithm caused a significant increase in performance when compared to not having any form of path reduction, and a simplistic reduction method.