Improving Symbolic Execution via Targeted Program Transformations

通过有针对性的程序转换改进符号执行

• 批准号: EP/N007166/1
• 负责人: Cristian Cadar
• 金额: $ 36.5万
• 依托单位: Imperial College London
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2016
• 资助国家: 英国
• 起止时间: 2016 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FN007166%2F1
• 关键词: Improving; Symbolic; Execution; via; Targeted

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.

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

项目成果

Computing summaries of string loops in C for better testing and refactoring

• DOI: 10.1145/3314221.3314610
• 发表时间: 2019-06
• 期刊: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
• 作者: Timotej Kapus;Oren Ish-Shalom;Shachar Itzhaky;N. Rinetzky;Cristian Cadar

A segmented memory model for symbolic execution

用于符号执行的分段内存模型

• DOI: 10.1145/3338906.3338936
• 发表时间: 2019
• 作者: Kapus T

Fine-Grain Memory Object Representation in Symbolic Execution

符号执行中的细粒度内存对象表示

• DOI: 10.1109/ase.2019.00089
• 发表时间: 2019
• 作者: Nowack M

Combining symbolic execution and search-based testing for programs with complex heap inputs

将符号执行和基于搜索的测试相结合，对具有复杂堆输入的程序进行测试

• DOI: 10.1145/3092703.3092715
• 发表时间: 2017
• 作者: Braione P

Accelerating array constraints in symbolic execution

• DOI: 10.1145/3092703.3092728
• 发表时间: 2017-07
• 期刊: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis
• 作者: D. Perry;Andrea Mattavelli;X. Zhang;Cristian Cadar