Article ID Journal Published Year Pages File Type
434409 Science of Computer Programming 2007 22 Pages PDF
Abstract

Static program analysis consists of compile-time techniques for determining properties of programs without actually running them. Using Kleene algebra, we formalize four instances of a general class of static intraprocedural data flow analyses known as ‘gen/kill’ analyses. This formalization exhibits the dualities between the four analyses in a clear and concise manner. We provide two equivalent sets of equations characterizing the four analyses for two different representations of programs, one in which the statements label the nodes of a control flow graph and one in which the statements label the transitions. We formally describe how the data flow equations for the two representations are related. We also prove the soundness of the KA based approach with respect to the standard approach.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics