Skip to main content

Enhancing the CBMC symbolic execution tool to support mixed concrete + symbolic execution

Supervisor

Suitable for

MSc in Computer Science

Abstract

The purpose of this enhancement is to solve cases where pure symbolic execution fails (incomplete decision procedures and handling of native libraries) while still maintaining its advantages. Previous work in [1] and [2] have mixed concrete and symbolic execution by using run time values of program variables to simplify constraints that could not be handled previously, or using concrete solutions of the solvable constraints in the current symbolic path condition. The project would involve implementing an approach similar to [2] into the existing CBMC tool.

[1] P. Godefroid, N.Klarlund, and K.Sen. DART: Directed Automated Random Testing. SIGPLAN Not., 40(6):213-223, 2005. [2] C. Pasareanu, N. Rungta, and W. Visser, Symbolic Execution with Mixed Concrete-Symbolic Solving. In International Symposium on Software Testing and Analysis (ISSTA), July 2011.