Tuesday September 4
08:30–09:00 Opening
09:00–10:00 Joint keynote talk by Prof. Moshe Vardi: The Siren Song of Temporal Synthesis
10:00–11:00 Runtime Verification & Enforcement
10:00–10:30 Luca Aceto, Ian Cassar, Adrian Francalanza and Anna Ingolfsdottir: On Runtime Enforcement via Suppressions
10:30–11:00 Radu Grigore and Stefan Kiefer: Selective Monitoring
11:00–11:30 Coffee break
11:30–13:00 Verification
11:30–12:00 Bernhard Kragl, Shaz Qadeer and Thomas A. Henzinger: Synchronizing the Asynchronous
12:00–12:30 Nima Roohi, Pavithra Prabhakar and Mahesh Viswanathan: Relating Syntactic and Semantic Perturbations of Hybrid Automata
12:30–13:00 Andrey Gorlin and C. R. Ramakrishnan: Separable GPL: decidable model checking with more non-determinism
13:00–14:30 Lunch break
14:30–16:00 Fairness, Serialisability, and Divergence
14:30–15:00 Tyler Sorensen, Hugues Evrard and Alastair Donaldson: GPU schedulers: how fair is fair enough?
15:00–15:30 Kartik Nagar and Suresh Jagannathan: Automated Detection of Serializability Violations under Weak Consistency
15:30–16:00 Shaull Almagor, Mehran Hosseini, Joel Ouaknine, James Worrell and Brynmor Chapman: Effective Divergence Analysis for Linear Recurrence Sequences
16:00–16:30 Coffee break
16:30–18:00 Cryptocurrency, Valence Systems, and Axiomatisation
16:30–17:00 Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen and Yaron Velner: Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-Currencies
17:00–17:30 Roland Meyer, Sebastian Muskalla and Georg Zetzsche: Bounded Context Switching for Valence Systems
17:30–18:00 Amina Doumane and Damien Pous: Completeness for Identity-free Kleene Lattices
18:30–20:30 Dinner
Wednesday September 5
08:30–09:25 Keynote talk by Prof. Yuxin Deng: Bisimulations for Probabilistic and Quantum Processes
09:25–09:30 CONCUR 2019 highlights
09:30–11:00 Synthesis
09:30–10:00 Véronique Bruyère, Quentin Hautem and Jean-Francois Raskin: Parameterized complexity of games with monotonically ordered w-regular objectives
10:00–10:30 Rodica Condurache, Youssouf Oualhadj and Nicolas Troquard: The Complexity of Concurrent Rational Synthesis
10:30–11:00 Ronny Tredup and Christian Rosenke: Narrowing down the Hardness Barrier of Synthesizing Elementary Nets
11:00–11:30 Coffee break
11:30–22:30 Lunch/Excursion/Banquet
Thursday September 6
08:30–09:30 Keynote talk by Prof. Rob van Glabbeek: Is speed-independent mutual exclusion implementable?
09:30–11:00 Co-Algebra
09:30–10:00 Tomasz Brengos: A coalgebraic take on regular and ω-regular behaviour for systems with internal moves
10:00–10:30 Barbara König and Christina Mika-Michalski: (Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras
10:30–11:00 Filippo Bonchi, Barbara König and Daniela Petrisan: Up-To Techniques for Behavioural Metrics via Fibrations
11:00–11:30 Coffee break
11:30–13:00 Petri Nets
11:30–12:00 Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr and Patrick Totzke: Universal Safety for Timed Petri Nets is PSPACE-complete
12:00–12:30 Benjamin Cabrera, Tobias Heindel, Reiko Heckel and Barbara König: Updating Probabilistic Knowledge on Condition/Event Nets using Bayesian Networks
12:30–13:00 Wojciech Czerwinski, Sławomir Lasota, Roland Meyer, Sebastian Muskalla, K Narayan Kumar and Prakash Saivasan: Regular Separability of Well-Structured Transition Systems
13:00–14:30 Lunch break
14:30–16:00 Timed Automata
14:30–15:00 Paul Gastin, Sayan Mukherjee and B Srivathsan: Reachability in timed automata with diagonal constraints
15:00–15:30 Massimo Bartoletti, Laura Bocchi and Maurizio Murgia: Progress-preserving Refinements of CTA
15:30–16:00 Krishna S, Khushraj Madnani and Paritosh Pandya: Logics meet 1-clock Alternating Automata: On Expressive, yet Decidable Real-time Logics
16:00–16:30 Coffee break
16:30–17:30 Bi-Simulation
16:30–17:00 Stephanie Balzer, Frank Pfenning and Bernardo Toninho: A Universal Session Type for Untyped Asynchronous Communication
17:00–17:30 Qiyi Tang and Franck van Breugel: Deciding Probabilistic Bisimilarity Distance One for Probabilistic Automata
17:45–18:30 Soccer match
18:30–20:30 Dinner
Friday September 7
08:30–09:30 Keynote talk by Prof. Bow-Yaw Wang: Verifying Assembly Codes for Practical Cryptography
09:30–11:00 Semantics
09:30–10:00 Jure Kukovec, Igor Konnov and Josef Widder: Reachability in Parameterized Systems: All Flavors of Threshold Automata
10:00–10:30 Benedikt Bollig, Marie Fortin and Paul Gastin: It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before"
10:30–11:00 Sergey Goncharov, Julian Jakob and Renato Neves: A Semantics for Hybrid Iteration
11:00–11:30 Coffee break
11:30–13:00 VAS / Weighted Automata
11:30–12:00 Piotr Hofman and Sławomir Lasota: Linear Equations with Ordered Data
12:00–12:30 Michael Blondin, Christoph Haase and Filip Mazowiecki: Affine Extensions of Integer Vector Addition Systems with States
12:30–13:00 Jakub Michaliszyn and Jan Otop: Non-deterministic Weighted Automata on Random Words
13:00–14:30 Lunch break
14:30–16:00 Probabilistic Systems
14:30–15:00 Jan Křetínský, Guillermo Perez and Jean-Francois Raskin: Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints
15:00–15:30 Paulin Fournier and Hugo Gimbert: Alternating Nonzero Automata
15:30–16:00 Jan Křetínský and Alexej Rotar: The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL
16:00–16:30 Coffee break
16:30–18:00 Quantitative Analysis
16:30–17:00 Michael Blondin, Javier Esparza and Antonin Kucera: Automatic Analysis of Expected Termination Time for Population Protocols
17:00–17:30 Javier Esparza, Pierre Ganty and Rupak Majumdar: Verification of Immediate Observation Population Protocols
17:30–18:00 Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar and Prakash Saivasan: Verifying Quantitative Temporal Properties of Procedural Programs
18:30–20:30 Dinner

Prof. Moshe Vardi: The Siren Song of Temporal Synthesis

One of the most significant developments in the area of design verification over the last three decade is the development of algorithmic methods for verifying temporal specification of finite-state designs. A frequent criticism against this approach, however, is that verification is done after significant resources have already been invested in the development of the design. Since designs invariably contains errors, verification simply becomes part of the debugging process. The critics argue that the desired goal is to use temporal specification in the design development process in order to guarantee the development of correct designs. This is called temporal synthesis. In this talk I will review 60 years of research on the temporal synthesis problem, describe the automata-theoretic approach developed to solve this problem, and describe both successes and failures of this research program.

Moshe Y. Vardi is the George Distinguished Service Professor in Computational Engineering and Director of the Ken Kennedy Institute for Information Technology at Rice University. He is the recipient of three IBM Outstanding Innovation Awards, the ACM SIGACT Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the Blaise Pascal Medal, the IEEE Computer Society Goode Award, the EATCS Distinguished Achievements Award, the Southeastern Universities Research Association's Distinguished Scientist Award, and the Church Award. He is the author and co-author of over 500 papers, as well as two books: "Reasoning about Knowledge" and "Finite Model Theory and Its Applications". He is a Fellow of the Association for Computing Machinery, the American Association for Artificial Intelligence, the American Association for the Advancement of Science, the European Association for Theoretical Computer Science, the Institute for Electrical and Electronic Engineers, and the Society for Industrial and Applied Mathematics. He is a member of the US National Academy of Engineering and National Academy of Science, the American Academy of Arts and Science, the European Academy of Science, and Academia Europaea. He holds honorary doctorates from the Saarland University in Germany, Orleans University in France, UFRGS in Brazil, and the University of Liege in Belgium. He is currently a Senior Editor of of the Communications of the ACM, after having served for a decade as Editor-in-Chief.

Prof. Yuxin Deng: Bisimulations for Probabilistic and Quantum Processes

Bisimulation is a fundamental concept in concurrency theory for comparing the behaviour of nondeterministic processes. It admits nice characterisations in many different ways such as fixed point theory, modal logics, game theory, coalgebras etc. In this talk, we review some key ideas used in the formulations and characterisations of reasonable notions of bisimulations for both probabilistic and quantum processes. To some extent the transition from probabilistic to quantum concurrency theory is smooth and natural. However, new ideas need also to be introduced. We have not yet reached the stage of formally verifying quantum communication protocols and quantum algorithms using bisimulations implemented by automatic tools. We discuss some recent efforts in this direction.

Yuxin Deng received his BEng (1999) and MSc (2002) from Shanghai Jiao Tong University, China, and PhD (2005) from Ecole des Mines de Paris, France. He was a research associate at University of New South Wales, Australia (2005-2006), an associate Professor at Shanghai Jiao Tong University, China (2006-2015), a visiting research fellow at Carnegie Mellon University, USA (2011), and a seconded expert at UNESCO Headquarters, France (2012-2014). In 2015 he joined East China Normal University as a full Professor. Dr. Deng’s research interests include concurrency theory, especially about process calculi, and formal semantics of programming languages, as well as formal verification of security protocols and distributed algorithms. He authored a book on the semantics of probabilistic processes.

Prof. Rob van Glabbeek: Is speed-independent mutual exclusion implementable?

A mutual exclusion algorithm is called speed independent if its correctness does not depend on the relative speed of the components. Famous mutual exclusion protocols such as Dekker's, Peterson's and Lamport's bakery are meant to be speed independent.
In this talk I argue that speed-independent mutual exclusion may not be implementable on standard hardware, depending on how we believe reading and writing to a memory location is really carried out. It can be implemented on electrical circuits, however.
This builds on previous work showing that mutual exclusion cannot be accurately modelled in standard process algebras.

Rob van Glabbeek has a strong international reputation in the study of the theory of concurrent computation, having made particular contributions to the conciliation of the interleaving and the true concurrency communities by codeveloping the current view of branching time and causality as orthogonal but interacting dimensions of concurrency. Some of his well known contributions are the linear time-branching time spectrum, branching bisimulation (with Peter Weijland), and action refinement (with Ursula Goltz). More recently, since 2015, he has worked with Peter Höfner on the notion of justness and on the (im)possibility of specifying fair schedulers or mutual exclusion protocols in standard process algebras. In addition, he has organised workshops on combining compositionality and concurrency, on logic, language and information, on the Unified Modelling Language, on workflow management, web services and business process modelling, on automatic and semi-automatic system verification, on structural operational semantics, and on formal methods for embedded systems. He is editor-in-chief of Electronic Proceedings in Theoretical Computer Science, a member of the editorial boards of Information and Computation and Theoretical Computer Science, and has been on several dozen program committees.

Prof. Bow-Yaw Wang: Verifying Assembly Codes for Practical Cryptography

Mathematical constructs are necessary for computation on the underlying algebraic structures of cryptosystems. They are often written in assembly languages and optimized manually for efficiency. We develop a hybrid technique to verify mathematical constructs implemented by assembly codes in OpenSSL and boringSSL. Our technique translates an algebraic specification of mathematical constructs into an algebraic problem. The algebraic problem in turn is solved by the computer algebra system Singular. The technique also translates overflow and range checking into the bit vector theory in SMT solvers. We report our case studies on verifying arithmetic computation over a large finite field in Curve25519 and NIST P-256, and the Montgomery Ladderstep in X25519.

Bow-Yaw Wang is a Research Fellow in Institute of Information Science, Academia Sinica, Taiwan. He was an Associate Research Fellow at Academia Sinica from 2008 to 2012, an INRIA Invited Professor from 2009 to 2011, an Invited Associate Professor at Tsinghua University from 2009 to 2010, an Adjoint Associate Professor at National Taiwan University from 2009 to 2012, an Assistant Research Fellow at Academia Sinica from 2003 to 2008, and an Adojoint Assistant Professor at National Taiwan University from 2004 to 2009. His research interest is logic and its application in computer science. He mainly works on formal verification. In the past, he has been working on compositional reasoning, program verification, learning-based verification techniques. More recently, he is interested in verifying assembly implementations of cryptographic primitives from security libraries such as OpenSSL and boringSSL. He is also running an interdisciplinary privacy research project at Academia Sinica.