Improving Symbolic Execution via Targeted Program Transformations

动态符号执行（DSE）在过去十年中获得了极大的普及，成为许多计算机科学领域（包括软件工程、编程语言、软件测试、验证、安全性和计算机系统）的标准技术工具箱的一部分。该技术支持广泛的应用程序，包括自动检测错误和安全漏洞、恢复损坏的文档、生成补丁和自动调试等等。DSE的有效性和可扩展性在很大程度上取决于程序的结构。也就是说，语义等价的程序在DSE探索程序状态空间的有效性方面可能存在很大差异。因此，本项目旨在发现和设计自动保持语义的程序转换，以提高DSE的可伸缩性。

Dynamic symbolic execution (DSE) has gained tremendous popularity in the last decade, becoming part of the standard toolbox of techniques in many computer science fields including software engineering, programming languages, software testing, verification, security, and computer systems. The technique has enabled a wide range of applications, including the automatic detection of bugs and security vulnerabilities, recovery of corrupt documents, patch generation, and automatic debugging, among many others.The effectiveness and scalability of DSE is highly dependent on the structure of the program. That is, semantically-equivalent programs can differ substantially with respect to the effectiveness of DSE to explore the program state space. As a result, this project aims to discover and design automatic semantics-preserving program transformations that improve the scalability of DSE.