1 DART is for directed automated random testing. Unit testing is good but so hard and expensive in practice, that it is rarely done properly. Three main techniques:

• automated extraction of the interface of a program with its external environment using static source-code parsing;
• automatic generation of a test driver for random testing;
• dynamic analysis based on that random and direct execution along alternative paths. Concolic?

DART is all of them. Implemented for C code. 2 They call DSE directed search (dynamically gather knowledge about the execution of the program). Research, which solver can return model without free variables. Path constraint represents an equivalence class of inputs. 3 Here is good theory on program and symbolic execution. Input specification is a sequence of addresses. We can change initial input during analysis. Execution tree. The goal of DART is to explore all path. Good luck! They support only the theory of integer linear constraints. When expression falls outside the theory, DART simply falls back to the concrete value. In two cases: (1) not linear and (2) tainted pointer dereference we raise incompleteness flag. I think, implicit flow does not imply incompleteness. We should prove it. They use term stack for prediction: with elements (then-branch or else-branch, was inverted or not).

4 Their algorithm: we start DSE (inner loop); when it ends, we checks completeness; if there was non-linear or tainted pointer dereference, we choose new random input and start DSE again (outer loop). What? There is always incompleteness on the real programs. Their invariant: last stack element is not inverted. They preserve input elements not involved in path constraint. Z3 can do that.

The theorem: DART will (1) found a bug; (2) or explore all paths; (3) or run forever. Oh! That's great! Theorem about nothing.

5 One of the advantages of DSE: it does not require alias analysis.

Sergey Vartanov, 2007–2020