Checking Assertions with Symbolic Pathfinder

Symbolic execution is a powerful analysis to systematically check assertions in programs. However, the already notorious scalability problem of symbolic execution is exacerbated by assertions. In our previous studies, we have introduced parallelism to check assertions with Symbolic Pathfinder (SPF) either with static analysis or dynamic analysis. In this work, we propose to combine static and dynamic analyses for parallel analysis to achieve better scalability, to further reduce the cost of symbolic execution using compositional and incremental assertion checking with SPF when the code or assertions are changed.