Outline

lecture
hall		 MON
Sept 12		 TUE
Sept 13		 WED
Sept 14		 THU
Sept 15		 FRI
Sept 16
1.007/8 Express/SOS CONCUR
3.017 SNR FMICS
1.012 YR CONCUR FORMATS
3.014 Trends QEST

Detailed program

Program

13.09.

CONCUR FORMATS QEST
08:55 – Opening 08:55 – Opening 08:55 – Opening
09:00 – Session 1: Invited lecture 09:00 – Invited talk 09:00 – Keynote talk
09:00
10:00
Concurrent Separation Logics: Logical Abstraction, Logical Atomicity and Environment Liveness Conditions
Philippa Gardner
09:00
10:00
A Behaviour-based Approach to Quantitative Validation of Cyber-Physical Systems
Thao Dang
09:00
10:00
Marta Kwiatkowska
10:00–10:30 Coffee break
10:30 – Session 2: Process algebra & semantics 10:30 – Probabilistic and Timed Systems 10:30 – Program Analysis
10:30
11:00
On the Axiomatisation of Branching Bisimulation Congruence over CCS
Luca Aceto, Valentina Castiglioni, Anna Ingolfsdottir and Bas Luttik
10:30
11:00
Bounded delay timed channel coding
Bernardo Jacobo Inclán, Eugene Asarin and Aldric Degorre.
10:30
11:00
Moment-based Invariants for Probabilistic Loops with non-polynomial assignments
Andrey Kofnov, Marcel Moosbrugger, Miroslav Stankovič, Ezio Bartocci and Efstathia Bura ( best paper award )
11:00
11:30
Non-Deterministic Abstract Machines
Malgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet and Alan Schmitt
11:00
11:30
Robustly Complete Finite-State Abstractions for Verification of Stochastic Systems
Yiming Meng and Jun Liu.
11:00
11:30
Distribution Estimation for Probabilistic Loops
Ahmad Karimi, Marcel Moosbrugger, Miroslav Stankovič, Laura Kovács, Ezio Bartocci and Efstathia Bura
11:30
12:00
Slimming Down Petri Boxes: Compact Petri Net Models of Control Flows
Victor Khomenko, Maciej Koutny and Alex Yakovlev
11:30
12:00
Model checking for entanglement swapping
Surya Sai Teja Desu, Anubhav Srivastava and Mvprao.
11:30
12:00
An Automated Quantitative Information Flow Analysis for Concurrent Programs
Khayyam Salehi, Ali A. Noroozi, Sepehr Amir-Mohammadian and Mohammadsadegh Mohagheghi
12:00–14:00 Lunch break
14:00 – Session 3: Stochastic models 14:00 – Temporal Logic 14:00 – Parameter Synthesis
14:00
14:30
On the Sequential Probability Ratio Test in Hidden Markov Models
Oscar Darwin and Stefan Kiefer
14:00
14:30
An STL-based Formulation of Resilience in Cyber-Physical Systems
Hongkai Chen, Shan Lin, Scott Smolka and Nicola Paoletti.
14:00
14:30
Rate Lifting for Stochastic Process Algebra - Exploiting Structural Properties
Markus Siegle and Amin Soltanieh
14:30
15:00
Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications
Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joel Ouaknine, David Purser, Markus Whiteland and James Worrell
14:30
15:00
MITL Verification Under Timing Uncertainty
Daniel Selvaratnam, Michael Cantoni, Jen Davoren and Iman Shames.
14:30
15:00
End-to-end Statistical Model Checking for Parametric ODE Models
David Julien, Guillaume Cantin and Benoît Delahaye
15:00
15:30
Anytime Guarantees for Reachability in Uncountable Markov Decision Processes
Kush Grover, Jan Kretinsky, Tobias Meggendorfer and Maximilian Weininger
15:00
15:30
Classification of driving behaviors using STL formula: A Comparative Study
Ruya Karagulle, Nikos Arechiga, Jonathan DeCastro and Necmiye Ozay.
15:00
15:30
POMDP Controllers With Optimal Budget
Jip Spel, Svenja Stein and Joost-Pieter Katoen
15:30–16:00 Coffee break
16:00 – Session 4: Timed systems 16:00 – Markovian Agents and Population Models
16:00
16:30
Checking timed Büchi automata emptiness using the local-time semantics
Frédéric Herbreteau, B Srivathsan and Igor Walukiewicz
16:00
16:30
A Logical Framework for Reasoning about Local and Global Properties of Collective Systems
Michele Loreti and Aniqa Rehman
16:30
17:00
Simulations for Event-Clock Automata
S Akshay, Paul Gastin, R Govind and B Srivathsan
16:30
17:00
Jump Longer to Jump Less: Improving Dynamic Boundary Projection with h-scaling
Francesca Randone, Luca Bortolussi and Mirco Tribastone
17:00 – Dynamical Systems
17:00
17:30
History-deterministic Timed Automata
Thomas Henzinger, Karoliina Lehtinen and Patrick Totzke
17:00
17:30
An Algorithm for the Formal Reduction of Differential Equations as Over-approximations
Giuseppe Squillace, Mirco Tribastone, Max Tschaikowski and Andrea Vandin
17:30
18:00
Decidability of One-Clock Weighted Timed Games with Arbitrary Weights
Benjamin Monmege, Julie Parreaux and Pierre-Alain Reynier
17:30
18:00
Stability Analysis of Planar Probabilistic Piecewise Constant Derivative Systems
Spandan Das (remote) and Pavithra Prabhakar
18:00–20:00 Reception

14.09.

CONCUR FMICS FORMATS QEST
09:00 – Session 5: Invited lecture 09:00 – Keynote 09:00 – Invited talk 09:00 – Keynote talk
09:00
10:00
Distributed Decision Problems: Concurrent Specifications beyond Binary Relations
Sergio Rajsbaum
09:00
09:05
Opening
Marieke Huisman
09:00
10:00
The Skolem Landscape
Joël Ouaknine
09:00
10:00
Pedro R. D'Argenio
09:05
10:00
Reinforcement Learning with Guarantees that Hold for Ever
Sven Schewe
10:00–10:30 Coffee break
10:30 – Session 6: Vector addition systems 10:30 – Certification 10:30 – Timed Automata and Games 10:30 – Tools
10:30
11:00
Language Inclusion for Boundedly-Ambiguous Vector Addition Systems is Decidable
Wojciech Czerwiński and Piotr Hofman
10:30
11:00
Formal Monotony Analysis of Neural Networks with Mixed Inputs: An asset for certification
Guillaume Vidot, Melanie Ducoffe, Christophe Gabreau, Ileana Ober and Iulian Ober
10:30
11:00
Timed Games with Bounded Window Parity Objectives
James C. A. Main, Mickael Randour and Jeremy Sproston.
10:30
11:00
LN: a Meta-Solver for Layered Queueing Network Analysis
Giuliano Casale, Yicheng Gao, Zifeng Niu and Lulai Zhu
11:00
11:30
Complexity of Coverability in Depth-Bounded Processes
A. R. Balasubramanian
11:00
11:30
Generating Interactive Validation Documents
Fabian Vu, Christopher Happe and Michael Leuschel
11:00
11:30
Non-Blind Strategies in Timed Network Congestion Games
Aline Goeminne, Nicolas Markey and Ocan Sankur.
11:00
11:30
LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning
Mohammadhosein Hasanbeig (remote), Daniel Kroening and Alessandro Abate
11:30
12:00
Determinization of One-Counter Nets
Shaull Almagor and Asaf Yeshurun
11:30
12:00
Deductive Verification of Smart Contracts with Dafny
Franck Cassez, Joanne Fuller and Horacio Mijail Anton Quiles
11:30
12:00
Efficient Convex Zone Merging in Parametric Timed Automata
Étienne André, Dylan Marinho, Laure Petrucci and Jaco van de Pol.
11:30
12:00
Eulero: A Tool for Quantitative Modeling and Evaluation of Complex Workflows
Laura Carnevali, Riccardo Reali (remote) and Enrico Vicario
12:00–14:00 Lunch break
14:00 – Session 7: Games I 14:00 – Industrial use cases 14:00 – FORMATS 20th Anniversary Session 14:00 – Applications
14:00
14:30
Energy Games with Resource-Bounded Environments
Orna Kupferman and Naama Shamash Halevy
14:00
14:30
Towards Reusable Formal Models for Custom Real-time Operating Systems
Julius Adelt, Julian Gebker and Paula Herber
14:00
14:30
Zone-based verification of timed automata: Extrapolations, simulations and what next?
Patricia Bouyer.
14:00
14:30
Analysis of an Electric Vehicle Charging System along a Highway
Davide Cerotti, Simona Mancini, Marco Gribaudo and Andrea Bobbio
14:30
15:00
Half-Positional Objectives Recognized by Deterministic Büchi Automata
Patricia Bouyer, Antonio Casares, Mickael Randour and Pierre Vandenhove
14:30
15:00
Formal Verification of an Industrial UML-like Model using mCRL2
Anna Stramaglia and Jeroen J.A. Keiren
14:30
15:00
A Personal History of Formal Modeling and Analysis of Timed Systems before there was FORMATS.
Thomas A. Henzinger.
14:30
15:00
Verifier's Dilemma in Ethereum Blockchain: A Quantitative Analysis
Daria Smuseva, Ivan Malakhov, Andrea Marin, Aad van Moorsel and Sabina Rossi
15:00
15:30
Two-player Boudedness Counter Games
Edwin Hamel-de le Court and Emmanuel Filiot
15:00
15:30
Chemical Case Studies in KeYmaera X
Rose Bohrer
15:00
15:30
On-line Testing and Monitoring of Real-Time Systems
Kim Guldstrand Larsen.
15:00
15:30
Comparing Statistical and Analytical Routing Approaches for Delay-Tolerant Networks
Pedro R. D'Argenio, Juan A. Fraire, Arnd Hartmanns and Fernando Raverta
15:30
16:00
Different strokes in randomised strategies: Revisiting Kuhn's theorem under finite-memory assumptions
James C. A. Main and Mickael Randour
15:30
16:00
Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining
Jana Berger, Wiebke Lenze, Thomas Noll, Simon Schotten, Thorsten Büker, Mario Fietze and Bastian Kogel
15:30
16:00
Preference-Aware Computation Offloading for IoT in Multi-Access Edge Computing Using Probabilistic Model Checking
Kaustabha Ray (remote) and Ansuman Banerjee
16:00 – The best paper award and further announcements. Marieke Huisman
16:00–19:00 Excursion
19:00–22:00 Banquet

15.09.

CONCUR FMICS FORMATS QEST
09:00 – Session 8: Invited lecture 09:00 – Keynote
09:00
10:00
Sequential Decision Making with Information Asymmetry
Rupak Majumdar
09:00
10:00
Supporting Railway Innovations with Formal Modelling and Verification
Bas Luttik
10:00–10:30 Coffee break
10:30 – Session 9: Verification 10:30 – Testing and monitoring 10:30 – Neural Networks 10:30 – Automata Theory and Applications
10:30
11:00
Regular Model Checking Upside-Down: An Invariant-Based Approach
Javier Esparza, Mikhail Raskin and Christoph Welzel
10:30
11:00
Test Suite Augmentation for Reconfigurable PLC Software in the Internet of Production
Marco Grochowski, Marcus Völker and Stefan Kowalewski
10:30
11:00
Neural Network Repair with Reachability Analysis
Xiaodong Yang, Tom Yamaguchi, Hoang-Dung Tran, Bardh Hoxha, Taylor T Johnson and Danil Prokhorov.
10:30
11:00
Mirrors and Memory in Quantum Automata
Carla Piazza and Riccardo Romanello
11:00
11:30
On an Invariance Problem for Parameterized Concurrent Systems
Marius Bozga, Lucas Bueri and Radu Iosif
11:00
11:30
Monitoring of Spatio-Temporal Properties with nonlinear SAT solvers
André De Matos Pedro, Tomás Silva, Tiago Sequeira, João M. Lourenço, João Costa Seco and Carla Ferreira
11:00
11:30
On Neural Network Equivalence Checking using SMT Solvers
Charis Eleftheriadis, Nikolaos Kekatos, Panagiotis Katsaros and Stavros Tripakis.
11:00
11:30
Monte Carlo Tree Search for Priced Timed Automata
Peter Gjøl Jensen, Andrej Kiviriga, Kim Guldstrand Larsen, Ulrik Nyman, Adriana Mijacika and Jeppe Høiriis Mortensen
11:30 – Best Paper Award and Closing Remarks
11:30
12:00
Towards Concurrent Quantitative Separation Logic
Ira Fesefeldt, Joost-Pieter Katoen and Thomas Noll
11:30
12:00
Model-Based Testing of Internet of Things Protocols
Xavier van Dommelen, Machiel van der Bijl and Andy Pimentel
11:30
12:00
Reachability Analysis of a General Class of Neural Ordinary Differential Equations
Diego Manzanas Lopez, Patrick Musau, Nathaniel Hamilton and Taylor T Johnson.
12:00–14:00 Lunch break
14:00 – Session 10: Languages & logics 14:00 – Methodology 14:00 – Reinforcement Learning
14:00
14:30
Completeness Theorems for Kleene Algebra with Top
Damien Pous and Jana Wagemaker
14:00
14:30
Formally Verifying Decompositions of Stochastic Specifications
Anton Hampus and Mattias Nyberg
14:00
14:30
Robust Event-Driven Interactions in Cooperative Multi-Agent Learning
Daniel Jarne Ornia and Manuel Mazo Jr.
14:30
15:00
Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties
Laura Bozzelli, Adriano Peron and Cesar Sanchez
14:30
15:00
Verification of Behavior Trees using Linear Constrained Horn Clauses
Thomas Henn, Marcus Völker, Stefan Kowalewski, Minh Trinh, Oliver Petrovic and Christian Brecher
14:30
15:00
Learning that grid convenience does not hurt resilience
Mathis Niehage and Anne Remke.
15:00
15:30
Propositional dynamic logic and asynchronous cascade decompositions for regular trace languages
Bharat Adsul, Paul Gastin, Saptarshi Sarkar and Pascal Weil
15:00
15:30
A Multi-level Methodology for Behavioral Comparison of Software-Intensive Systems
Dennis Hendriks, Arjan van der Meer and Wytse Oortwijn
15:30–16:00 Coffee break
16:00 – Session 11: Test of Time award + Best paper award + Business meeting
16:00
16:15
Approximate symbolic model checking of continuous-time Markov chains (CONCUR 1999)
Joost-Pieter Katoen
16:15
16:30
The Impressive Power of Stopwatches (CONCUR 2000)
Franck Cassez
16:30
16:45
Deriving Bisimulation Congruences for Reactive Systems (CONCUR 2000)
James Leifer
16:45
17:30
The Element of Surprise in Timed Games (CONCUR 2003)
Luca de Alfaro And Marco Faella

16.09.

CONCUR
09:00 – Session 12: Invited lecture
09:00
10:00
Reachability in Vector Addition Systems by Examples
Wojciech Czerwiński
10:00–10:30 Coffee break
10:30 – Session 13: Concurrency
10:30
11:00
A Kleene Theorem for Higher-Dimensional Automata
Uli Fahrenberg, Christian Johansen, Georg Struth and Krzysztof Ziemiański
11:00
11:30
Diamonds for Security: A Non-Interleaving Operational Semantics for the Applied Pi-Calculus
Clément Aubert, Ross Horne and Christian Johansen
11:30
12:00
Weak Progressive Forward Simulation is Necessary and Sufficient for Strong Observational Refinement
Brijesh Dongol, Gerhard Schellhorn and Heike Wehrheim
12:00–14:00 Lunch break
14:00 – Session 14: Games II
14:00
14:30
Concurrent Games with Multiple Topologies
Shaull Almagor and Shai Guendelman
14:30
15:00
Strategies for MDP Bisimilarity Equivalence and Inequivalence
Stefan Kiefer and Qiyi Tang
15:00
15:30
Pareto-Rational Verification
Véronique Bruyère, Jean-Francois Raskin and Clément Tamines
15:30–16:00 Coffee break
16:00 – Session 15: Session types
16:00
16:30
Generalised Multiparty Session Types with Crash-Stop Failures
Adam D. Barwell, Alceste Scalas, Nobuko Yoshida and Fangyi Zhou
16:30
17:00
An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear π-Calculus
Luca Ciccone and Luca Padovani
17:00
17:30
On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments
Ugo Dal Lago and Giulia Giusti