CAREER: Scalable Dynamic Program Reasoning

Purdue University, West Lafayette IN

Investigators

Abstract

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.