Reference:

Dejvuth Suwimonteerabuth. Reachability in pushdown systems: Algorithms and applications. PhD thesis, Technische Universität München, 2009.

Abstract:

This thesis presents reachability algorithms for pushdown systems and their applications to different areas. Roughly speaking, a pushdown system is a stack-based machine whose stack can be unbounded, making it a natural model for sequential programs. Inspired by applications, the thesis analyzes reachability in more generalized pushdown models—alternating pushdown systems and pushdown networks—and discusses their complexities in detail. A pushdown network can be used for modeling multithreaded programs. The reachability algorithms, together with a translator from Java bytecodes into pushdown networks, have been optimized and implemented in a tool called jMoped. jMoped is an Eclipse plug-in which allows users to easily test Java programs without any knowledge of the techniques behind it. jMoped progressively outputs coverability information and uncovers errors such as assertion violations. Several practical experiments with jMoped are reported. Alternating pushdown systems are shown to be suitable models for authorization systems and reputation systems, where reasoning in the systems boils down to solving reachability in the models.

Suggested BibTeX entry:

@phdthesis{Suw09,
    author = {Dejvuth Suwimonteerabuth},
    school = {Technische Universit\"at M\"unchen},
    title = {Reachability in Pushdown Systems: Algorithms and Applications},
    year = {2009}
}