Improving Symbolic Execution via Targeted Program Transformations

点击翻译按钮获取中文摘要

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.