Describing data flow analysis techniques with Kleene algebra

摘要

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.