Enhancing the CBMC symbolic execution tool to support mixed concrete + symbolic execution
AbstractThe 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  and  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  into the existing CBMC tool.
 P. Godefroid, N.Klarlund, and K.Sen. DART: Directed Automated Random Testing. SIGPLAN Not., 40(6):213-223, 2005.  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.