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 tree-structured infinite data alphabet, called split automata, whose distinctive feat...