### 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:

- Conventional dataflow-analysis algorithms merge together the values for all states associated with the same program point, regardless of the states' calling context. With the dataflow-analysis algorithm obtained via weighted PDSs, dataflow queries can be posed with respect to a regular language of stack configurations. Conventional merged dataflow information can also be obtained by issuing appropriate queries; thus, the new approach provides a strictly richer framework for interprocedural dataflow analysis than is provided by conventional interprocedural dataflow-analysis algorithms.
- Because the algorithm for solving path problems in weighted PDSs can provide a witness set of paths, it is possible to provide an explanation of why the answer to a dataflow query has the value reported.

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].