Verifying higher-order concurrency with data automata

Using a combination of automata-theoretic and game-semantic techniques, we propose a method for analysing higher-order concurrent programs. Our language of choice is Finitary Idealised Concurrent Algol (FICA) due to its relatively simple fully abstract game model.

Our first contribution is an automata model over a treestructured infinite data alphabet, called split automata, whose distinctive feature is the separation of control and memory. We show that every FICA term can be translated into such an automaton. Thanks to the structure of split automata, we are able to observe subtle aspects of the underlying game semantics.

This enables us to identify a fragment of FICA with iteration and limited synchronisation (but without recursion), for which, in contrast to the whole FICA, a variety of verification problems turn out to be decidable.