Staged Symbolic Execution for Parallel Property Checking

While annotating functional correctness properties of code, e.g., using assertions, enables automated conformance checking of program behaviors to expected properties and has found its use in many bug finding techniques, efficiently checking properties in practice remains challenging. In this paper, we introduce a novel approach to distributing checking properties using staged symbolic execution, which consists of two stages: (1) the first stage searches for all feasible paths to the checked properties as targets for the second stage, and (2) the second stage distributes property checking along these target paths among multiple workers, each focusing on one or more paths depending on the available computing resources. We implement our approach on top of Symbolic PathFinder, and our experience with our approach in checking assertions annotated in two Java programs shows its effectiveness