DART - Directed Automated Random Testing
This paper describes DART, the concolic execution engine that CUTE built upon. This paper is pretty old (2005), so it uses different vocabulary than what I'm used to.
The paper starts by describing the state of correctness checking at the time. It
notes that random testing is generally effective, but usually provides low
code coverage. It makes the interesting observation that the conditional
if (x == 10) has a 1/232 chance of being executed, but I think
that this is often irrelevant. It seems to emphasize that DART is API-agnostic,
which is probably less interesting now than it was at the time. It identifies
some of the tools it aims to replace: Prefix/Prefast, MC, Klocwork, and Polyspace.
I haven't heard of any of those so maybe it was successful.
The paper next explains the general approach of DART, which I summarized in my post on CUTE. Then, it goes on to explain Dart's implementation and usage, which I won't cover. An interesting note is that it describes the operational semantics in prose instead of the notation that's common now.
In the implementation section, it also includes some proofs about various aspects of DART. I don't know a lot about constraint solvers, but the authors note that they assume the solver can only solve linear constraints, and use this to explain "how to handle the transition from constraints within the theory to those that are outside."
In the additional remarks section, the authors note that they assumed that any functions called in external libraries have no side effects on the heap. They also assumed that all variables are initialized, which they note can be checked easily by static analysis.
Next, they note DART's advantages over static analysis, which are pretty expected. Then, they include experimental results and conclude.
This post is a bit less shorter than the last because I covered most of the interesting bits of DART in my last post on CUTE. Next time I should probably go in chronological order.