Evènement pour le groupe Séminaire Méthodes Formelles


Date 2021-05-04  07:00-07:00
TitreVerifying higher-order concurrency with data automata 
Résumé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 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. This is joint work with Alex Dixon (Warwick), Ranko Lazic (Warwick) and Igor Walukiewicz (Bordeax), to appear at LiCS’21. I will also discuss earlier related work from FoSSaCS’21 Recording: https://u-bordeaux-fr.zoom.us/rec/share/IC3Uv_FTVnghe5s_7rpTzqwzCdKo27G0IgjZyZY8az-ehFCdSYgbBwNY8-fX7eeJ.sf6r4vpSXb1A--Z8 
LieuOnline 
OrateurAndrzej Murawski 
Emailhttps://www.cs.ox.ac.uk/people/andrzej.murawski/ 
UrlUniversity of Oxford 



Aucun document lié à cet événement.

Retour
Retour à l'index