Module 11: Symbolic Execution with a Graph Database

Faculty Contact: Tevfik Bultan and Xifeng Yan

Research Areas:

Symbolic execution is a program analysis technique that has become very influential and has been applied to many challenging problems in software verification, software analysis and computer security. The enabling technology for the recent success of symbolic execution techniques has been advanced decision procedures, called Satisfiability-Modula-Theories (SMT) solvers, that check satisfiability of complex constraints. One bottleneck in symbolic execution is efficient processing of repeated calls to constraint solvers. One approach is to store the calls to constraint solvers in a database and reuse them. In this work module we would like to investigate the use of graph databases for efficient constraint storage. We envision that the students who work on this module will look at the interface between a well-known symbolic execution tool for Java bytecode called Symbolic PathFinder (SPF) and a constraint database called Green, and investigate the feasibility of replacing Green with a graph database

Here are some related papers and tools:

* A symbolic execution tool:
"Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis"
Corina S. Păsăreanu, Willem Visser, David Bushnell, Jaco Geldenhuys, Peter Mehlitz, Neha Rungta. Automated Software Engineering, September 2013, Volume 20, Issue 3, pp 391-425.

Symbolic PathFinder:

* A constraint database for symbolic execution:
"Green: reducing, reusing and recycling constraints in program analysis"
Willem Visser, Jaco Geldenhuys and Matthew B. Dwyer Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, Article No. 58. The Green Solver

The Green Solver:

* Graph databases and graph processing platform:
Neo4j Cayley Spark/GraphX (it is a distributed graph processing platform)

Through this project, we evaluate these systems and determine which one is appropriate for supporting/replacing Green.

Active Quarters

  • Winter 2016, Tegan Brennan