The Library
Verifying higher-order concurrency with data automata
Tools
Tools
Tools
Dixon, Alex, Lazic, Ranko, Murawski, Andrzej S. and Walukiewicz, Igor (2021) Verifying higher-order concurrency with data automata. In: ACM/IEEE LICS 2021 : 36th Annual Symposium on Logic in Computer Science, Virtual conference, 29 Jun - 2 Jul 2021. Published in: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) ISBN 9781665448963. doi:10.1109/LICS52264.2021.9470691
|
PDF
WRAP-Verifying-higher-order-concurrency-data-automata-Dixon-2021.pdf - Accepted Version - Requires a PDF viewer. Download (1364Kb) | Preview |
Official URL: https://doi.org/10.1109/LICS52264.2021.9470691
Abstract
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.
| Item Type: | Conference Item (Paper) | ||||||
|---|---|---|---|---|---|---|---|
| Subjects: | Q Science > QA Mathematics > QA75 (Please use QA76 Electronic Computers. Computer Science) | ||||||
| Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||||
| Library of Congress Subject Headings (LCSH): | Parallel programming (Computer science) -- Semantics, Game-theoretical semantics, Algorithms, Semantics -- Data processing, Computer programming, Machine theory, Game theory -- Computer programs | ||||||
| Journal or Publication Title: | 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) | ||||||
| Publisher: | IEEE | ||||||
| ISBN: | 9781665448963 | ||||||
| Official Date: | 7 July 2021 | ||||||
| Dates: |
|
||||||
| DOI: | 10.1109/LICS52264.2021.9470691 | ||||||
| Status: | Peer Reviewed | ||||||
| Publication Status: | Published | ||||||
| Reuse Statement (publisher, data, author rights): | © 2021 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. | ||||||
| Access rights to Published version: | Restricted or Subscription Access | ||||||
| Date of first compliant deposit: | 5 May 2021 | ||||||
| Date of first compliant Open Access: | 16 September 2021 | ||||||
| RIOXX Funder/Project Grant: |
|
||||||
| Conference Paper Type: | Paper | ||||||
| Title of Event: | ACM/IEEE LICS 2021 : 36th Annual Symposium on Logic in Computer Science | ||||||
| Type of Event: | Conference | ||||||
| Location of Event: | Virtual conference | ||||||
| Date(s) of Event: | 29 Jun - 2 Jul 2021 | ||||||
| Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
 |
View Item |
Downloads
Downloads per month over past year
