dc.contributor.author Lin, Yude dc.date.accessioned 2018-01-25T04:23:23Z dc.date.available 2018-01-25T04:23:23Z dc.date.issued 2017 en_US dc.identifier.uri http://hdl.handle.net/11343/197985 dc.description © 2017 Dr. Yude Lin dc.description.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. en_US 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. dc.rights Terms and Conditions: Copyright in works deposited in Minerva Access is retained by the copyright owner. The work may not be altered without permission from the copyright owner. Readers may only download, print and save electronic copies of whole works for their own personal non-commercial use. Any use that exceeds these limits requires permission from the copyright owner. Attribution is essential when quoting or paraphrasing from these works. dc.subject symbolic execution en_US dc.subject test generation en_US dc.subject program verification en_US dc.title Symbolic execution with over-approximation en_US dc.type PhD thesis en_US melbourne.affiliation.department Computing and Information Systems melbourne.affiliation.faculty Engineering melbourne.thesis.supervisorname Miller, Tim melbourne.contributor.author Lin, Yude melbourne.accessrights Open Access
﻿