CAREER: Scalable Dynamic Program Reasoning

在软件工程中，动态分析是在程序执行过程中检查正确的程序行为。动态分析超越了分析、跟踪遍历和简单属性验证等传统功能。动态分析的更广泛的分支取决于满足称为动态推理的关键挑战，该挑战询问程序执行上的什么转换将导致属性的逻辑满足。例如，在数据竞争检测中，确定数据竞争是否是良性的可以转化为确定改变两个冲突的存储器访问的顺序是否影响输出。自动修补错误代码相当于查找更改，以便产生所需的输出。这项研究针对动态推理的一些关键挑战。新颖的规范表示便于对齐执行，特别是原始执行及其转换后的版本，因此可以在兼容的位置执行执行比较。高效的转换技术包括检查点设置长执行和有选择地扰动执行状态以观察可满足性。基于约束求解的推理引擎旨在将任意执行区域转换为符号约束，然后使用求解器来推理可满足性。使用动态切片来界定执行区域是实现可伸缩性的关键。在更广泛的影响中，肯定会有更正确的软件。

In software engineering, dynamic analysis is the checking of correct program behavior during program executions. Dynamic analysis is advancing beyond traditional capabilities such as profiling, trace traversing, and simple property verification. The broader ramifications of dynamic analysis hinge on meeting a key challenge called dynamic reasoning, which asks what transformations on a program execution would lead to logical satisfaction of the properties. For example, in data race detection, deciding whether a data race is benign can be translated into deciding if changing the order of the two conflicting memory accesses affects the output. Automatically patching faulty code is equivalent to looking for changes so that the desired output can be produced. This research targets a number of key challenges for dynamic reasoning. Novel canonical representations facilitate aligning executions, particularly the original execution and its transformed version, so that execution comparison can be performed at compatible places. Efficient transformation techniques include checkpointing long executions and selectively perturbing execution state to observe satisfiability. A reasoning engine based on constraint solving aims to translate an arbitrary execution region into symbolic constraints and then use a solver to reason about satisfiability. Using dynamic slicing to delimit the execution region is the key to scalability. Among the broader impacts will be certifiably more correct software.