Skip to content
University of Maryland LibrariesDigital Repository at the University of Maryland
    • Login
    View Item 
    •   DRUM
    • College of Computer, Mathematical & Natural Sciences
    • Computer Science
    • Technical Reports of the Computer Science Department
    • View Item
    •   DRUM
    • College of Computer, Mathematical & Natural Sciences
    • Computer Science
    • Technical Reports of the Computer Science Department
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Mixing Type Checking and Symbolic Execution (Extended Version)

    Thumbnail
    View/Open
    CS-TR-4954.pdf (310.1Kb)
    No. of downloads: 1030

    Date
    2010-03-23
    Author
    Khoo, Yit Phang
    Chang, Bor-Yuh Evan
    Foster, Jeffrey S.
    Metadata
    Show full item record
    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
    Collections
    • Technical Reports of the Computer Science Department

    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.
    Web Accessibility
     

     

    Browse

    All of DRUMCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

    My Account

    LoginRegister
    Pages
    About DRUMAbout Download Statistics

    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.
    Web Accessibility