Posts

Measuring the coverage achieved by symbolic execution

Cristian Cadar and Timotej Kapus This blog post is meant for symbolic execution users and developers who are interested in measuring the coverage achieved by a symbolic execution tool as a proxy for the effectiveness of a symbolic execution campaign.  We use KLEE as an example tool, but this discussion is applicable to other implementations as well.  We also use statement coverage in our discussion, but other forms of coverage raise similar issues.  Suppose you run KLEE on a program for a few hours and you want to measure the coverage achieved by KLEE in this time.  There are two main ways to achieve this: rely on the coverage reported by KLEE or measure the coverage externally using a tool such as GCov.  We describe each in turn and then discuss how they differ from one another and when each of them should be used. Coveraged measured internally ("internal coverage") The first option is to simply rely on the coverage reported by KLEE.  A tool like KLEE considers a statement