Blogs (28) >>
ECOOP 2016
Sun 17 - Fri 22 July 2016 Rome, Italy
Tue 19 Jul 2016 13:50 - 14:20 at Belli - Session 3 Chair(s): Davide Ancona

This article introduces ATAB, a tool that automatically generates pairwise reachability checks for action trees. Ac- tion trees can be used to study the behaviour of real-world concurrent programs. ATAB encodes pairwise reachability checks into alternating tree automata (ATA) that determine whether an action tree has a schedule where any pair of given points in the program are simultaneously reachable. Because the pairwise reachability problem is undecidable in general ATAB operates under a restricted form of lock-based concurrency. ATAB produces ATA that are more compact and more efficiently checkable than those that have been previously used. The process is entirely automated, which simplifies the process of encoding checks for more complex action trees. The ATA produced are easier to scale to large numbers of locks than previous constructions.

Tue 19 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:50 - 15:20
Session 3FTfJP at Belli
Chair(s): Davide Ancona University of Genova
13:50
30m
Talk
Generating Concurrency Checks Automatically
FTfJP
Jonathan Hoyland Royal Holloway University of London, Matthew Hague Royal Holloway University of London
14:20
30m
Talk
An Extended Buffered Memory Model With Full Reorderings
FTfJP
14:50
30m
Talk
Towards a Model of Corecursion with Default
FTfJP
Davide Ancona University of Genova, Francesco Dagnino , Elena Zucca University of Genova