LARA Pushdown systems Push down automaton and context-free grammars. Summary of results. Stefan Schwoon's thesis: Model-Checking Pushdown Systems R. Alur, M. Benedikt, K. Etessami, P. Godefroid, T. Reps, and M. Yannakakis. Analysis of Recursive State Machines