Mixing type checking and symbolic execution

Static analysis designers must carefully balance precision and efficiency. In our experience, many static analysis tools are built around an elegant, core algorithm, but that algorithm is then extensively tweaked to add just enough precision for the coding idioms seen in practice, without sacrificing too much efficiency. There are several downsides to adding precision in this way: the tool’s implementation becomes much more complicated; it can be hard for an end-user to interpret the tool’s results; and as software systems vary tremendously in their coding styles, it may require significant algorithmic engineering to enhance a tool to perform well in a particular software domain. In this paper, we present MIX, a novel system that mixes type checking and symbolic execution. The key aspect of our approach is that these analyses are applied independently on disjoint parts of the program, in an off-the-shelf manner. At the boundaries between nested type checked and symbolically ex...

• Type: Conference
• Year: 2010
• Where: PLDI
• Authors: Yit Phang Khoo, Bor-Yuh Evan Chang, Jeffrey S. Foster
• Keywords: PLDI 2010, Static Analysis, Symbolic Execution, Type Checking