Dissertation Proposal - Kenny Ballou

Exploiting Incrementality of Data-Flow Analysis to Reason About Zonotope Abstract Domains

Presented by Kenny Ballou, Computer Science emphasis
City Center Plaza Conference Room 368

Abstract

Developing correct, defect-free software for safety-critical systems is an important goal of software engineering. Static analysis is a powerful technique that proves the absence of defects. Since many safety-critical software uses numerical calculations, a special kind of static analysis that combines data-flow analysis and abstract interpretation is used to reason about those computations. Data-flow analysis propagates information, and abstract interpretation defines the type of information. One of the widely used types is a family of weakly-relational domains called Zonotopes, which includes the Intervals, Zones, and Octagons abstract domains. Computing Zonotope information scales poorly due to the numerous relations between variables encoded in the information. There exists a body of work on improving efficiency and effectiveness of algorithms over Zonotope information. However, this work is unique because it leverages the incremental nature of data-flow analysis to improve the results of Zonotope analyses.

The prior work explored incrementality in the context of the Zones weakly-relational domain. The first publication uses the canonical property of Zones to improve the performance of an important Zones operation used in data-flow analysis. The second work exploits incrementality for identifying minimal changed variables within a Zone abstract domain. The latest work uses the minimal changed variables within a minimal union algorithm for comparing information over weakly-relational abstract domains.

The proposal extends this prior work to the Octagons weakly-relational abstract domain. The first proposed objective is to develop an incremental, strong transitive closure algorithm, a necessary operation for comparison between two Octagon abstract states. The second objective is to create algorithms for minimally changed variables within an Octagon abstract state. The final objective is to extend the minimal union algorithm to consider abstract domain ordering to improve its efficiency and, ideally, reduce the number of variables necessary for comparing two weakly-relational abstract domains. The results of each objective will be empirically evaluated using Zones and Octagons over a set of established benchmark programs.

Committee

Dr. Elena Sherman (Chair), Dr. Jim Buffenbarger, Dr. Marion Scheepers