A Saturation Method for Collapsible Pushdown Systems

Photograph of Matthew Hague

Matthew Hague

(Université Paris-Est)

We study the model-checking problem for models of higher-order programs. In particular, via higher-order recursion schemes and their connection to collapsible pushdown systems. We present a saturation method for global backwards reachability analysis of these models. Beginning with an automaton representing a set of configurations, we build an automaton accepting all configurations that can reach this set. We also improve upon previous saturation techniques for higher-order pushdown systems by significantly reducing the size of the automaton constructed and simplifying the algorithm and proofs. This is joint work with C. Broadbent, A. Carayol and O. Serre in Paris.
Thursday 31st May 2012, 14:00
Far-134 (Video Conferencing Room)
Department of Computer Science