Pushdown systems (PDSs) are an automata-theoretic formalism for specifying a class of infinite-state transition systems. Infiniteness comes from the fact that each configuration in the state space consists of a (formal) ``control location'' p coupled with a stack S of unbounded size. PDSs can model program paths that have matching calls and returns, and automaton-based representations allow analysis algorithms to account for the infinite control state space of recursive programs.

Weighted pushdown systems (WPDSs) are a generalization of PDSs that add a general ``black-box'' abstraction for program data (through weights). WPDSs also generalize other frameworks for interprocedural analysis, such as the Sharir-Pnueli functional approach.

This paper surveys recent work in this area, and establishes a few new connections with existing work.

(Click here to access the paper: PDF; (c) Springer-Verlag.)