Weighted Pushdown Systems and their Application to Interprocedural Dataflow Analysis

This work has established new connections between interprocedural dataflow analysis and model checking of pushdown systems (PDSs). Various connections between dataflow analysis and model checking have been established in past work, e.g., [S91, S93, S98, EK99, CC00]; however, with one exception ([EK99]), past work has shed light only on the relationship between model checking and bit-vector dataflow-analysis problems, such as live-variable analysis and partial-redundancy elimination. In contrast, the results obtained in our work [RSJ03, RSJM] apply to (i) bit-vector problems, (ii) the one non-bit-vector problem addressed in [EK99], as well as (iii) certain dataflow-analysis problems that cannot be expressed as bit-vector problems, such as linear constant propagation SRH96 and affine-relation analysis MOS04. In general, the approach can be applied to any distributive dataflow-analysis problem for which the domain of transfer functions has no infinite descending chains. (Safe solutions are also obtained for problems that are monotonic but not distributive.)

The contributions of the work can be summarized as follows:

The algorithms described in [RSJ03, RSJM] are implemented in the open-source library WALi: the Weighted Automata Library.

Weighted pushdown systems are also a useful formalism in a completely separate application domain, namely, access control of shared computing resources in distributed systems [JR04, SJRS03, JR02, JSWR06, WJRSS06].