Improving the performance of symbolic execution to make it scale to industrial-sized programs is an important current issue. Veritesting provides a practical solution by combining the advantages of static symbolic execution (SSE) with those of dynamic symbolic execution (DSE). While Avgerinos et al. showed veritesting allows large-scale testing at the X86 binary level, it can also be applied to improve the performance of dynamic symbolic execution at the Java bytecode level. Symbolic PathFinder (SPF) performs symbolic execution for Java programs at the bytecode level. In this project, I plan to work on extending Symbolic PathFinder (SPF) to perform bounded static symbolic execution.


Vaibhav B Sharma


  • Mike
  • Willem Visser