Mixing type checking and symbolic execution

13 years 9 months ago

Download www.cs.umd.edu

Static analysis designers must carefully balance precision and efﬁciency. 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 sacriﬁcing too much efﬁciency. 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 signiﬁcant 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

Real-time Traffic