Show simple item record

dc.contributor.authorLin, Yude
dc.date.accessioned2018-01-25T04:23:23Z
dc.date.available2018-01-25T04:23:23Z
dc.date.issued2017en_US
dc.identifier.urihttp://hdl.handle.net/11343/197985
dc.description© 2017 Dr. Yude Lin
dc.description.abstractProgram 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.en_US
dc.rightsTerms 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.subjectsymbolic executionen_US
dc.subjecttest generationen_US
dc.subjectprogram verificationen_US
dc.titleSymbolic execution with over-approximationen_US
dc.typePhD thesisen_US
melbourne.affiliation.departmentComputing and Information Systems
melbourne.affiliation.facultyEngineering
melbourne.thesis.supervisornameMiller, Tim
melbourne.contributor.authorLin, Yude
melbourne.accessrightsOpen Access


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record