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.