Kleene Algebra and Bytecode Verification
Cornell University Ithaca United States
Pagination or Media Count:
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 6 we introduced 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 data flow labeling is not achieved by inductively labeling the program with abstract values, but rather by computing the star Kleene closure of a matrix of transfer functions. In this paper we show how this general framework applies to the problem of Java bytecode verification. We show how to specify transfer functions arising in Java bytecode verification in such a way that the Kleene algebra operations join, composition, star can be computed efficiently. We also give a hybrid dataflow analysis algorithm that computes the closure of a matrix on a cutset of the control flow graph, thereby avoiding the recalculation of dataflow information when there are cycles in the graph. This method could potentially improve the performance over the standard worklist algorithm when a small cutset can be found.