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 automat...
Main Authors: | Dixon, A, Lazić, R, Murawski, AS, Walukiewicz, I |
---|---|
Format: | Conference item |
Language: | English |
Published: |
IEEE
2021
|
Similar Items
-
Leafy automata for higher-order concurrency
by: Dixon, A, et al.
Published: (2021) -
Verifying Determinism of Concurrent Systems Which Use Unbounded Arrays
by: Roscoe, A, et al.
Published: (1998) -
Third-order Idealized Algol with iteration is decidable
by: Murawski, A, et al.
Published: (2008) -
Saturating automata for game semantics
by: Dixon, A, et al.
Published: (2023) -
Weak Alternating Timed Automata
by: Pawel Parys, et al.
Published: (2012-09-01)