Banner of Newcastle upon Tyne Famous Bridges


Conference Programme


09.00-09.30 Opening session

09.30-10.30 Invited talk
Peter Sewell
False Concurrency and Strange-but-True Machines

10.30-11.00 Coffee

11.00-12.30 Reachability analysis
Béatrice Bérard, Serge Haddad, Mathieu Sassolas and Nathalie Sznajder
Concurrent Games on VASS with Inhibition
Wojciech Czerwiński, Piotr Hofman and Sławomir Lasota
Reachability Problem for Weak Multi-pushdown Automata
Nengkun Yu and Mingsheng Ying
Reachability and Termination Analysis of Concurrent Quantum Programs

12.30-14.00 Lunch

14.00-16.00 Qualitative and timed systems
Guy Avni and Orna Kupferman
Making Weighted Containment Feasible: A Heuristic Based on Simulation and Abstraction
Sandie Balaguer and Thomas Chatain
Avoiding Shared Clocks in Networks of Timed Automata
Krishnendu Chatterjee, Mickael Randour and Jean-François Raskin
Strategy Synthesis for Multi-dimensional Quantitative Objectives
Emmanuel Filiot, Raffaella Gentilini and Jean-François Raskin
Quantitative Languages Defined by Functional Automata

16.00-16.30 Coffee

16.30-17.30 Behavioural equivalences
Romain Brenguier, Stefan Göller and Ocan Sankur
A Comparison of Succinctly Represented Finite-State Systems
Antti Valmari
All Linear-Time Congruences for Familiar Operators Part 2: Infinite LTSs

19.00-20.00 Welcome reception


09.00-10.00 Invited talk
Brian Randell
A Turing Enigma

10.00-10.30 Coffee

10.30-11.30 Temporal logics
Arnaud Da Costa, Francois Laroussinie and Nicolas Markey
Quantified CTL: Expressiveness and Model Checking
Fabio Mogavero, Aniello Murano, Giuseppe Perelli and Moshe Vardi
What Makes ATL* Decidable? A Decidable Fragment of Strategy Logic

11.30-12.30 Session types
Tzu-Chun Chen and Kohei Honda
Specifying Stateful Asynchronous Properties for Distributed Programs
Julien Lange and Emilio Tuosto
Synthesising Choreographies from Local Session Types

12.30-14.00 Lunch

14.00-15.00 Abstraction
Fides Aarts, Faranak Heidarian and Frits Vaandrager
A Theory of History Dependent Abstractions for Learning Interface Automata
Alexey Gotsman and Hongseok Yang
Linearizability with Ownership Transfer

15.00-15.30 Coffee

17.00-22.00 Excursion & dinner


09.00-10.00 Invited talk
Jos Baeten
Turing Meets Milner

10.00-10.30 Coffee

10.30-12.30 Mobility and space in process algebras
Romain Demangeon and Kohei Honda
Nested Protocols in Session Types
Luca Fossati, Kohei Honda and Nobuko Yoshida
Intensional and Extensional Characterisation of Global Progress in the Pi-calculus
Daniel Hirschkoff, Jean-Marie Madiot and Davide Sangiorgi
Duality and i/o-types in the Pi-calculus
Sophia Knight, Catuscia Palamidessi, Prakash Panangaden and Frank Valencia
Spatial and Epistemic Modalities in Constraint-Based Process Calculi

12.30-14.00 Lunch

14.00-16.00 Stochastic systems
Luca Bortolussi and Jane Hillston
Fluid Model Checking
Taolue Chen, Vojtech Forejt, Marta Kwiatkowska, Aistis Simaitis, Ashutosh Trivedi and Michael Ummels
Playing Stochastic Games Precisely
Mark Timmer, Joost-Pieter Katoen, Jaco Van De Pol and Marielle I A Stoelinga
Efficient Modelling and Generation of Markov Automata
Max Tschaikowski and Mirco Tribastone
Exact Fluid Lumpability for Markovian Process Algebra

16.00-16.30 Coffee

16.30-17.30 Probabilistic systems
Daniel Gebler and Wan Fokkink
Compositionality of Probabilistic Hennessy-Milner Logic through Structural Operational Semantics
Henning Kerstan and Barbara König
Coalgebraic Trace Semantics for Probabilistic Transition Systems Based on Measure Theory


09.00-10.00 Invited talk
Gordon Plotkin
Concurrency and the Algebraic Theory of Effects

10.00-10.30 Coffee

10.30-12.30 Petri nets and non-sequential semantics
Ryszard Janicki, Xiang Yin and Nadezhda Zubkova
Modeling Interval Order Structures with Partially Commutative Monoids
Roland Meyer, Victor Khomenko and Reiner Huechting
A Polynomial Translation of Pi-calculus (FCP) to Safe Petri Nets
Łukasz Mikulski
Algebraic Structure of Combined Traces
Cesar Rodriguez and Stefan Schwoon
Verification of Petri Nets with Read Arcs

12.30-14.00 Lunch

14.00-16.00 Verification
Matthias Függer and Josef Widder
Efficient Checking of Link-reversal-based Concurrent Systems
Alexander Kaiser, Daniel Kroening and Thomas Wahl
Efficient Coverability Analysis by Proof Minimization
Mohsen Lesani, Victor Luchangco and Mark Moir
A Framework for Formally Verifying Software Transactional Memory Algorithms
Roy Mennicke
Propositional Dynamic Logic with Converse and Repeat for Message-Passing Systems

16.00-16.30 Coffee

16.30-17.30 Decidability
Aiswarya Cyriac, Paul Gastin and K Narayan Kumar
MSO Decidability of Multi-Pushdown Systems via Split-Width
Frank de Boer, Cosimo Laneve, Gianluigi Zavattaro and Mahdi Jaghoori
Decidability Problems for Actor Systems

17.30-18.00 Closing session