Verifying higher-order concurrency with data automata

Using a combination of automata-theoretic and game-semantic techniques, we give a new method for analysing higher-order concurrent programs. Our language of choice is Finitary Idealised Concurrent Algol (FICA). Our first contribution is an automata model over a tree-structured 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 FICA itself, a variety of verification problems turn out to be decidable. In the presentation, we shall discuss FICA, the construction of Split Automata, some of the decidability results we have shown on our FICA fragment, and the consequences for the analysis of higher-order concurrent programs. The presentation will be of broad interest to those in the fields of game semantics, automata theory, and programming language theory. This is joint work with Ranko Lazic, Andrzej S. Murawski and Igor Walukiewicz.

Authors

• Alex Dixon

Keywords

No keywords are indexed for this paper.