Model checking pushdown processes

Javier Esparza,
University of Stuttgart
Friday, 14 November, 2003 (All day)

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 started to work on the analysis of pushdown processes in 1997. At that time our motivation was purely theoretical. Six years later, our work (and what we have drawn from the work of others) has produced the Moped tool, a model-checker for pushdown systems able to find bugs in Windows XP drivers with 27000 lines of code.

In this talk I'll sketch the (rather long) way from the theory to the realisation. I will spend some time explaining the basic ideas, and then present some experimental results. I'll then sketch some other applications.

This is joint work with Stefan Schwoon