Compositional symbolic execution with memoized replay

Simple item page
dc.contributor.advisorKhurshid, Sarfraz
dc.contributor.advisorYang, Guowei
dc.creatorQiu, Rui, active 21st centuryen
dc.date.accessioned2014-09-18T19:54:42Zen
dc.date.accessioned2018-01-22T22:26:31Z
dc.date.available2018-01-22T22:26:31Z
dc.date.issued2014-05en
dc.date.submittedMay 2014en
dc.date.updated2014-09-18T19:54:42Zen
dc.descriptiontexten
dc.description.abstractSymbolic execution is a powerful, systematic analysis that has received much visibility in the last decade. Scalability however remains a major challenge for symbolic execution. Compositional analysis is a well-known general purpose methodology for increasing scalability. This thesis introduces a new approach for compositional symbolic execution. Our key insight is that we can summarize each analyzed method as a memoization tree that captures the crucial elements of symbolic execution, and leverage these memoization trees to efficiently replay the symbolic execution of the corresponding methods with respect to their calling contexts. Memoization trees offer a natural way to compose in the presence of heap operations, which cannot be dealt with by previous work that uses logical formulas as summaries for composi- tional symbolic execution. Our approach also enables an efficient treatment of error traces by short-circuiting the execution of paths that lead to them. Our preliminary experimental evaluation based on a prototype implementation in Symbolic PathFinder shows promising results.en
dc.description.departmentElectrical and Computer Engineeringen
dc.format.mimetypeapplication/pdfen
dc.identifier.urihttp://hdl.handle.net/2152/26006en
dc.language.isoenen
dc.subjectCompositionalen
dc.subjectSymbolic executionen
dc.subjectProgram analysisen
dc.subjectHeap operationen
dc.titleCompositional symbolic execution with memoized replayen
dc.typeThesisen

Files

Collections

University of Texas at Austin