Extending SPF with handling of symbolic arrays, and implementing a replay module

Symbolic Pathfinder (SPF) is an open-source symbolic execution tool, based on NASA Java Pathfinder (JPF) model checker, which is used in research and industry labs. It executes Java bytecode using a custom JVM to perform its analysis. We propose to add support for symbolic execution of complex datastructures, especially arrays, and to implement a module to generate concrete inputs and replay symbolic execution with concrete variables.