Compositional symbolic execution with memoized replay
| dc.contributor.advisor | Khurshid, Sarfraz | |
| dc.contributor.advisor | Yang, Guowei | |
| dc.creator | Qiu, Rui, active 21st century | en |
| dc.date.accessioned | 2014-09-18T19:54:42Z | en |
| dc.date.issued | 2014-05 | en |
| dc.date.submitted | May 2014 | en |
| dc.date.updated | 2014-09-18T19:54:42Z | en |
| dc.description | text | en |
| dc.description.abstract | Symbolic 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.department | Electrical and Computer Engineering | en |
| dc.format.mimetype | application/pdf | en |
| dc.identifier.uri | http://hdl.handle.net/2152/26006 | en |
| dc.language.iso | en | en |
| dc.subject | Compositional | en |
| dc.subject | Symbolic execution | en |
| dc.subject | Program analysis | en |
| dc.subject | Heap operation | en |
| dc.title | Compositional symbolic execution with memoized replay | en |
| dc.type | Thesis | en |
| thesis.degree.department | Electrical and Computer Engineering | en |
| thesis.degree.discipline | Electrical and Computer Engineering | en |
| thesis.degree.grantor | The University of Texas at Austin | en |
| thesis.degree.level | Masters | en |
| thesis.degree.name | Master of Science in Engineering | en |