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.

Organization

Student

afromherz

Mentors

  • Corina
  • Luckow
close

2016