故障导向程序修剪（扩展版）
Failure-Directed Program Trimming (Extended Version)
摘要：
本文介绍了一种新的程序简化技术，称为程序修剪，旨在提高安全检查工具的可扩展性和精度。给定程序${\mathcal P}$，程序修整生成新程序${\mathcal P}'$，使得${\mathcal P}$和${\mathcal P}'$是同等安全的（即，${\mathcal P}'$有bug当且仅当${\mathcal P}$有bug时），但${\mathcal P}'$的执行路径比${\mathcal P}$少。由于许多程序分析器是敏感的执行路径的数量，程序修剪有可能提高安全检查工具的有效性。除了引入程序修剪的概念，本文还提出了一个轻量级的静态分析，可以作为一个预处理步骤，删除程序路径，同时保持等安全性。我们已经实现了所提出的技术在一个工具，称为修剪和评估它的上下文中的两个程序分析技术，即抽象解释和动态符号执行。我们的实验表明，程序修剪显着提高了这两种技术的有效性。
英文摘要：
This paper describes a new program simplification technique called program trimming that aims to improve the scalability and precision of safety checking tools. Given a program ${\mathcal P}$, program trimming generates a new program ${\mathcal P}'$ such that ${\mathcal P}$ and ${\mathcal P}'$ are equi-safe (i.e., ${\mathcal P}'$ has a bug if and only if ${\mathcal P}$ has a bug), but ${\mathcal P}'$ has fewer execution paths than ${\mathcal P}$. Since many program analyzers are sensitive to the number of execution paths, program trimming has the potential to improve the effectiveness of safety checking tools. In addition to introducing the concept of program trimming, this paper also presents a lightweight static analysis that can be used as a pre-processing step to remove program paths while retaining equi-safety. We have implemented the proposed technique in a tool called Trimmer and evaluate it in the context of two program analysis techniques, namely abstract interpretation and dynamic symbolic execution. Our experiments show that program trimming significantly improves the effectiveness of both techniques.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
