Parallel Property Checking with Symbolic Execution
Junye Wen, Guowei Yang · Proceedings/Proceedings of the ... International Conference on Software Engineering and Knowledge Engineering · 2018
Systematically checking code against functional correctness properties is costly, especially for complex code annotated with rich behavioral properties.This paper introduces a novel approach to checking properties in parallel using symbolic execution.Our approach partitions a check for the whole set of properties into multiple simpler sub-checks-each sub-check focusing on a single property, so that different properties are checked in parallel among multiple workers.Furthermore, each sub-check is guided by the checked property to avoid exploring irrelevant paths and is prioritized based on distances towards the checked property to provide early feedback.We implement our approach in Symbolic PathFinder, and experiments on systematically checking assertions in Java programs show the effectiveness of our approach.