Model checking pushdown processes

Pushdown processes are pushdown automata seen under a different light: we are not interested in the languages they recognise, but in the transitions systems they generate. These are infinite transition systems with pairs of the form (control state, stack content) as states.

We use pushdown processes to model programs with (possibly recursive) procedures. We study the problem of checking if all the infinite executions of a pushdown process satisfy a formula of Linear Temporal Logic (LTL), and derive efficient algorithms. Applications to verification problems are discussed.

This is joint work with Stefan Schwoon