Accession Number:

AD1000906

Title:

Second-Order Abstract Interpretation via Kleene Algebra

Descriptive Note:

Technical Report

Corporate Author:

Cornell University Ithaca

Personal Author(s):

Report Date:

2004-12-01

Pagination or Media Count:

7.0

Abstract:

Most standard approaches to the static analysis of programs, such as the popular worklist method, are first-order methods that inductively annotate program points with abstract values. In this paper we introduce a second-order approach based on Kleene algebra. In this approach, the primary objects of interest are not the abstract data values, but the transfer functions that manipulate them. These elements form a left-handed Kleene algebra. The dataflow labeling is not achieved by inductively labeling the program with abstract values, but rather by computing the star Kleene closureof a matrix of transfer functions. In this paper we introduce the method and prove soundness and completeness with respect to the standard worklist algorithm.

Subject Categories:

  • Numerical Mathematics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE