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.
Descriptors:
Subject Categories:
- Numerical Mathematics