The Symbolic Execution (SPF) extension for NASA’s Java Pathfinder (JPF) has been used to generate quality test cases by symbolically executing code and using the derived constraints to find test values which will follow each feasible program path.

A similar idea views the derived constraints as a partial specification of correct program behavior and uses this data to guide program repair. This turns program repair into a search problem over the space of code snippets characterized by constraints derived via symbolic execution, the “semantic search” problem. Previous work in this area was done exclusively with C programs, and the extension of this work to Java would be of major benefit for program repair research.

For GSoC, I propose to use SPF to empirically quantify the degree to which such an approach is possible using currently-existing open-source Java programs, create functionality-searchable database of Java code snippets, and use this with existing efforts for search-based program repair.


Andrew Hill


  • Kasper Luckow
  • Corina
  • Divya Gopinath