Mixing type checking and symbolic execution

11 years 3 months ago
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...
Yit Phang Khoo, Bor-Yuh Evan Chang, Jeffrey S. Fos
Added 10 Jul 2010
Updated 10 Jul 2010
Type Conference
Year 2010
Where PLDI
Authors Yit Phang Khoo, Bor-Yuh Evan Chang, Jeffrey S. Foster
Comments (0)