In this paper, we reduce pushdown system (PDS) model checking to a graph-theoretic problem, and apply a fast graph algorithm to improve the running time for model checking. We use weighted PDSs as a generalized setting for PDS model checking, and show how various PDS model checkers can be encoded using weighted PDSs. We also give algorithms for witness tracing, differential propagation, and incremental analysis, each of which benefits from the fast graph-based algorithm.

(Click here to access the paper: PDF.)