• Login
    View Item 
    •   MINDS@UW Home
    • MINDS@UW Madison
    • College of Letters and Science, University of Wisconsin–Madison
    • Department of Computer Sciences, UW-Madison
    • CS Technical Reports
    • View Item
    •   MINDS@UW Home
    • MINDS@UW Madison
    • College of Letters and Science, University of Wisconsin–Madison
    • Department of Computer Sciences, UW-Madison
    • CS Technical Reports
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Symbolic Analysis via Semantic Reinterpretation

    Thumbnail
    File(s)
    TR1640.pdf (326.6Kb)
    Date
    2008
    Author
    Lim, Junghee
    Lal, Akash
    Reps, Thomas
    Publisher
    University of Wisconsin-Madison Department of Computer Sciences
    Metadata
    Show full item record
    Abstract
    In recent years, the use of symbolic analysis in systems for testing and verifying programs has experienced a resurgence. By ``symbolic program analysis'', we mean logic-based techniques to analyze state changes along individual program paths. The three basic primitives used in symbolic analysis are functions that perform forward symbolic evaluation, weakest precondition, and symbolic composition by manipulating formulas. The conventional approach to implementing systems that use symbolic analysis is to write each of the three symbolic-analysis functions by hand for the programming language of interest. In this paper, we develop a method to create implementations of these primitives so that they can be made available easily for multiple programming languages -- particularly for multiple machine-code instruction sets. In particular, we have created a system in which, for the cost of writing just one specification -- of the semantics of the programming language of interest, in the form of an interpreter expressed in a functional language -- one obtains automatically-generated implementations of all three symbolic-analysis functions. We show that this can be carried out even for programming languages with pointers, aliasing, dereferencing, and address arithmetic. The technique has been implemented, and used to automatically generate symbolic-analysis primitives for multiple machine-code instruction sets.
    Permanent Link
    http://digital.library.wisc.edu/1793/60644
    Type
    Technical Report
    Citation
    TR1640
    Part of
    • CS Technical Reports

    Contact Us | Send Feedback
     

     

    Browse

    All of MINDS@UWCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

    My Account

    Login

    Contact Us | Send Feedback