ParSym: Parallel symbolic execution

Scaling software analysis techniques based on source-code, such as symbolic execution and data flow analyses, remains a challenging problem for systematically checking software systems. The increasing availability of clusters of commodity machines provides novel opportunities to scale these techniques using parallel algorithms. This paper presents ParSym, a novel parallel algorithm for scaling symbolic execution using a parallel implementation. In every iteration ParSym explores multiple branches of a path condition in parallel by distributing them among available workers resulting in an efficient parallel version of symbolic execution. Experimental results show that symbolic execution is highly scalable using parallel algorithms: using 512 processors, more than two orders of magnitude speedup are observed.