Extending Path Merging for SPF

Path merging is a promising technique that speeds up dynamic symbolic execution by multiple factors. In Path merging expensive forking is minimized by statically analyzing and summarizing regions of code, which are then used during dynamic symbolic execution. This technique was first introduced by the name of Veritesting[1] for c programs and recently implemented for Java programs in Java Ranger [2]. Both works report substantial benefits from merging of paths, with the latter winning SVComp’2020, a competition among Java verification and analysis tools.

In this proposal, I plan to: 1) support test case generation for Java Ranger that would support branch coverage criteria, and 2) experiment the feasibility of path merging of threads by implementing a simulated thread interpreter and using Java Ranger to path merge thread interleavings.