Computer Sciences Dept.

Improving Pushdown System Model Checking

Akash Lal, Thomas Reps

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 \textit{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.

Download this report (PDF)

Return to tech report index

Computer Science | UW Home