University of Maryland DRUM  
University of Maryland Digital Repository at the University of Maryland

Digital Repository at the University of Maryland (DRUM) >
College of Computer, Mathematical & Natural Sciences >
Computer Science >
Technical Reports of the Computer Science Department >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1903/10115

Title: Mixing Type Checking and Symbolic Execution (Extended Version)
Authors: Khoo, Yit Phang
Chang, Bor-Yuh Evan
Foster, Jeffrey S.
Type: Technical Report
Issue Date: 23-Mar-2010
Series/Report no.: UM Computer Science Department;CS-TR-4954
Abstract: 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 executed code regions, we use special mix rules to communicate information between the off-the-shelf systems. The resulting mixture is a provably sound analysis that is more precise than type checking alone and more efficient than exclusive symbolic execution. In addition, we also describe a prototype implementation, Mixy, for C. Mixy checks for potential null dereferences by mixing a null/non-null type qualifier inference system with a symbolic executor
URI: http://hdl.handle.net/1903/10115
Appears in Collections:Technical Reports of the Computer Science Department

Files in This Item:

File Description SizeFormatNo. of Downloads
CS-TR-4954.pdf310.11 kBAdobe PDF538View/Open

All items in DRUM are protected by copyright, with all rights reserved.

 

DRUM is brought to you by the University of Maryland Libraries
University of Maryland, College Park, MD 20742-7011 (301)314-1328.
Please send us your comments