Show simple item record

dc.contributor.authorKot, Lucjaen_US
dc.contributor.authorKozen, Dexteren_US
dc.description.abstractMost 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 Kleene algebra. The dataflow 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 introduce the method and prove soundness and completeness with respect to the standard worklist algorithm.en_US
dc.format.extent160905 bytes
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleSecond-Order Abstract Interpretation via Kleene Algebraen_US
dc.typetechnical reporten_US

Files in this item


This item appears in the following Collection(s)

Show simple item record