Show simple item record

dc.contributor.advisorKhurshid, Sarfraz
dc.creatorYang, Guowei, active 2013en
dc.date.accessioned2013-09-20T14:44:46Zen
dc.date.issued2013-08en
dc.date.submittedAugust 2013en
dc.identifier.urihttp://hdl.handle.net/2152/21259en
dc.descriptiontexten
dc.description.abstractThe last few years have seen a resurgence of interest in the use of symbolic execution--program analysis technique developed more than three decades ago to analyze program execution paths. However, symbolic execution remains an expensive technique and scaling it remains a key technical challenge. There are two key factors that contribute to its cost: (1) the number of paths that need to be explored and (2) the cost of constraint solving, which is typically required for each path explored. Our insight is that the cost of symbolic execution can be reduced by an incremental approach, which uses static analysis and dynamic analysis to focus on relevant parts of code and reuse previous analysis results, thereby addressing both the key cost factors of symbolic execution. This dissertation presents Memoized Incremental Symbolic Execution, a novel approach that embodies our insight. Using symbolic execution in practice often requires several successive runs of the technique on largely similar underlying problems where successive problems differ due to some change, which may be to code, e.g., to fix a bug, to analysis parameters, e.g., to increase the path exploration depth, or to correctness properties, e.g., to check against stronger specifications that are written as assertions in code. Memoized Incremental Symbolic Execution, a three-fold approach, leverages the similarities in the successive problems to reduce the total cost of applying the technique. Our prototype tool-set is based on the Symbolic PathFinder. Experimental results show that Memoized Incremental Symbolic Execution enhances the efficacy of symbolic execution.en
dc.format.mimetypeapplication/pdfen
dc.language.isoen_USen
dc.subjectSymbolic executionen
dc.subjectIncremental analysisen
dc.subjectTrie data structureen
dc.subjectConstraint solvingen
dc.subjectProgram differencingen
dc.subjectAssertion differencingen
dc.subjectSoftware evolutionen
dc.titleEnhancing symbolic execution using memoization and incremental techniquesen
dc.date.updated2013-09-20T14:44:46Zen
dc.description.departmentElectrical and Computer Engineeringen
thesis.degree.departmentElectrical and Computer Engineeringen
thesis.degree.disciplineElectrical and Computer Engineeringen
thesis.degree.grantorThe University of Texas at Austinen
thesis.degree.levelDoctoralen
thesis.degree.nameDoctor of Philosophyen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record