Incremental SMT Solving for Symbolic Execution

Symbolic execution is a popular, though computationally expensive, program analysis technique with applications in software reliability. My bachelor’s thesis explored whether incremental SMT solving could enhance its performance. I was supervised by Dr. Cristian Cadar, whose guidance I deeply appreciate.

The algorithms and optimisations proposed were implemented in KLEE, an open-source symbolic execution engine written in C++. They yielded significant execution-time improvements over the state-of-the-art when benchmarked. A novel system for deterministically replaying randomised symbolic execution runs was also developed to ensure accurate comparisons of strategies.

(The research cannot be shared at this time, as we are working on its publication. Watch this space!)