University Library
  • Login
A gateway to Melbourne's research publications
Minerva Access is the University's Institutional Repository. It aims to collect, preserve, and showcase the intellectual output of staff and students of the University of Melbourne for a global audience.
View Item 
  • Minerva Access
  • Engineering and Information Technology
  • Computing and Information Systems
  • Computing and Information Systems - Theses
  • View Item
  • Minerva Access
  • Engineering and Information Technology
  • Computing and Information Systems
  • Computing and Information Systems - Theses
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

    Symbolic execution with over-approximation

    Thumbnail
    Download
    Thesis (1.582Mb)

    Citations
    Altmetric
    Author
    Lin, Yude
    Date
    2017
    Affiliation
    Computing and Information Systems
    Metadata
    Show full item record
    Document Type
    PhD thesis
    Access Status
    Open Access
    URI
    http://hdl.handle.net/11343/197985
    Description

    © 2017 Dr. Yude Lin

    Abstract
    Program verification is difficult but crucial in establishing software's reliability and security. As the software industry grows rapidly, traditional verification methods, such as code reviewing, inspection, and manual testing, become laborious and less effective. Symbolic Execution (SE) is an important automation technique in program verification. SE can analyse a program automatically and obtain information about the feasible paths in the program. For each such path SE captures the condition on the inputs to reach the path, as well as the corresponding program behaviour. SE has received much attention from researchers in the last decade, and is used effectively in the software industry. The biggest problems with symbolic execution are path explosion (efficiency) and the sophistication of program semantics or software systems (precision). In order to make SE scalable, existing SE approaches frequently use under-approximation---a class of techniques that narrow the search space of SE, such as concretisation and aggressive path pruning. This thesis shows that over-approximation can be more advantageous in some cases, especially when we can differentiate unimportant or irrelevant code from the more critical or interesting code. In our research, we study the strengths and weaknesses of over-approximation adaptations in SE. We introduce novel techniques based on two types of over-approximation, namely ``contextual'' and ``regional'' over-approximation. Contextual over-approximation focuses on symbolically executing specific parts of a program, while disregarding the context information; this particular feature makes results reusable, thus reducing SE redundancy. Regional over-approximation (over-approximating the details) can focus SE on program parts that are the most beneficial (e.g., implying the most code coverage), while disregarding irrelevant details. This saves the cost of SE when the code can be better differentiated, and shows great promise in targeted SE or proof-oriented applications. A drawback of techniques that use over-approximation is that they introduce infeasible program states which could mean false positives. The cost of eliminating such false positives is substantial. We show how incremental constraint solving techniques, in particular, assumption checking is a potential solution in this case. We base our discussion in this thesis on three innovative implementations of SE that centre around the above ideas.
    Keywords
    symbolic execution; test generation; program verification

    Export Reference in RIS Format     

    Endnote

    • Click on "Export Reference in RIS Format" and choose "open with... Endnote".

    Refworks

    • Click on "Export Reference in RIS Format". Login to Refworks, go to References => Import References


    Collections
    • Minerva Elements Records [52443]
    • Computing and Information Systems - Theses [404]
    Minerva AccessDepositing Your Work (for University of Melbourne Staff and Students)NewsFAQs

    BrowseCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects
    My AccountLoginRegister
    StatisticsMost Popular ItemsStatistics by CountryMost Popular Authors