Program

Below you will find the program for the ABZ 2021 virtual conference. All times are given in the GMT+2 (CEST) timezone. First, an overview of the entire week is provided, followed by a detailed program for each day. The days and the sessions are cross-linked, so you can jump from the overview directly to the detailed information and by clicking on the (sticky) day at the top of the page back to the overview.

When preparing your presentations, please keep in mind the following time frames for the different types of contributions:

Regarding the case study, a short introduction to the case study will be given by Frank Houdek at the beginning of the case study session. This way you can focus on the formalization specific parts in your presentation without introducing the case study itself.

Overview

GMT+2
8:30
9:00
9:30
10:00
10:30
11:00
11:30
12:00
12:30
13:00
13:30
14:00
14:30
15:00
15:30
16:00
16:30
17:00
17:30
18:00
Coffee Break
11:00 - 11:30 / wonder.me
Lunch
12:50 - 14:00 / wonder.me
Coffee Break
15:40 - 16:20 / wonder.me
Coffee Break
10:30 - 11:00 / wonder.me
Lunch
12:30 - 13:30 / wonder.me
Coffee Break
Coffee Break
10:30 - 11:00 / wonder.me
Lunch
12:30 - 13:30 / wonder.me
Coffee Break
15:30 - 16:00 / wonder.me
Coffee Break
10:50 - 11:20 / wonder.me
Lunch
12:20 - 13:30 / wonder.me
Coffee Break
15:30 - 16:00 / wonder.me
Coffee Break
10:45 - 11:15 / wonder.me
Lunch
12:30 - 13:15 / wonder.me
Coffee Break
Farewell
17:30 - 18:00 / zoom

Last updated: 2021-05-27

GMT+2
9:00
11:00
12:50
14:00
15:40
16:20
18:00
Session I Alexander Raschke
9:00 - 11:00 / zoom
9:00 Opening Klaus Dieter-Schewe, Elvinia Riccobene, Alexander Raschke
9:20 Some Thoughts on Computational Models: From Massive Human Computing to Abstract State Machines, and Beyond Johann A. Makowsky
9:40 Some Observations on Mitotic Sets Klaus Ambos-Spies
10:00 Communities and Ancestors Associated with Egon Börger and ASM Jonathan Bowen
10:20 Models and Modelling in Computer Science Bernhard Thalheim
Coffee Break
11:00 - 11:30 / wonder.me
Session II Klaus-Dieter Schewe
11:30 - 12:50 / zoom
11:30 A Framework for Modeling the Semantics of Synchronous and Asynchronous Procedures with Abstract State Machines Wolf Zimmermann, Mandy Weißbach
11:50 Flashix: Modular Verification of a Concurrent and Crash-Safe Flash File System Stefan Bodenmüller, Gerhard Schellhorn, Martin Bitterlich, Wolfgang Reif
12:10 The ASMETA Approach to Safety Assurance of Software Systems Paolo Arcaini, Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini, Elvinia Riccobene, Patrizia Scandurra
12:30 Spot the Difference: A Detailed Comparison Between B and Event-B Michael Leuschel
Lunch
12:50 - 14:00 / wonder.me
Session III Elvinia Riccobene
14:00 - 15:40 / zoom
14:00 Towards Leveraging Domain Knowledge in State-Based Formal Methods Yamine Ait Ameur, Régine Laleau, Dominique Méry, Neeraj Kumar Singh
14:20 Language and Communication Problems in Formalization: a Natural Language Approach Alessandro Fantechi, Stefania Gnesi, Laura Semini
14:40 Moded and Continuous Abstract State Machines Richard Banach, Huibiao Zhu
15:00 What is the Natural Abstraction Level of an Algorithm? Andreas Prinz
15:20 The Combined Use of the Web Ontology Language (OWL) and Abstract State Machines (ASM) for the Definition of a Specification Language for Business Processes Matthes Elstermann, André Wolski, Albert Fleischmann, Christian Stary, Stephan Borgert
Coffee Break
15:40 - 16:20 / wonder.me
Session IV Uwe Glässer
16:20 - 18:00 / zoom
16:20 Semantic Splitting of Conditional Belief Bases Christoph Beierle, Jonas Haldimann, Gabriele Kern-Isberner
16:40 ASM Specification and Refinement of a Quantum Algorithm Flavio Ferrarotti, Senén González
17:00 Analysis of Mobile Networks' Protocols Based on Abstract State Machines Emanuele Covino, Giovanni Pani
17:20 A Stepwise Design Optimization Problem Don Batory, Jeho Oh, Ruben Heradio, David Benavides
17:40 Computation on Structures: Behavioural Theory, Logic, Complexity Klaus-Dieter Schewe
GMT+2
9:00
10:30
11:00
12:30
13:30
15:00
15:30
17:30
9th Rodin User and Developer Workshop - Session 1 Asieh Salehi
09:00 - 10:30 / zoom
9:00 Opening and Welcome
9:10 Domain knowledge as Ontology-based Event-B Theories I. Mendil, Y. Aït-Ameur, N. K. Singh, D. Méry, and P. Palanque
9:30 OntoEventB: A Generator of Event-B contexts from Ontologies Idir Ait-Sadoune
9:50 EVBT — an Event-B tool for code generation and documentation Fredrik Öhrström
10:10 Scenario Checker: An Event-B tool for validating abstract models Colin Snook, Thai Son Hoang, Asieh Salehi Fathabadi, Dana Dghaym, Michael Butler
Coffee Break
10:30 - 11:00 / wonder.me
9th Rodin User and Developer Workshop - Session 2 Yamine Aït-Ameur
11:00 - 12:30 / zoom
11:00 Introduction
11:10 Context instantiation plug-in: a new approach to genericity in Rodin Guillaume Verdier, Laurent Voisin
11:30 Examples of using the Instantiation Plug-in Dominique Cansell, Jean-Raymond Abrial
11:50 Data-types definitions: Use of Theory and Context instantiations Plugins Peter Riviere, Yamine Ait-Ameur, and Neeraj Kumar Singh
12:10 Towards CamilleX 3.0 Thai Son Hoang, Colin Snook, Asieh Salehi Fathabadi, Dana Dghaym, Michael Butler
Lunch
12:30 - 13:30 / wonder.me
9th Rodin User and Developer Workshop - Session 3 Colin Snook
13:30 - 15:00 / zoom
13:30 Introduction
13:35 Keynote: Safety and Security Case Study Experiences with Event-B and Rodin Jonathan Hammond, Capgemini Engineering
14:20 Large Scale Biological Models in Rodin Usman Sanwal, Thai Son Hoang, Luigia Petre, and Ion Petre
14:40 Formal Verification of EULYNX Models Using Event-B and RODIN Abdul Rasheeq, Shubhangi Salunkhe
Coffee Break
15:00 - 15:30 / wonder.me
DSLs with Jetbrains MPS - Session 1
09:00 - 10:30 / zoom
DSLs with Jetbrains MPS - Session 2
11:00 - 12:30 / zoom
GMT+2
8:30
10:30
11:00
12:30
13:30
15:30
16:00
17:30
Session 1 Klaus-Dieter Schewe
08:30 - 10:30 / zoom
8:30 Welcome and Opening Alexander Raschke
8:45 Towards ASM-based automated formal verification of security protocols Chiara Braghin, Mario Lilli, Elvinia Riccobene
9:15 Proving the safety of a Sliding Window Protocol with Event B Sophie Coudert
9:45 Account and Transaction Protocol of the Open Banking Standard Abdul Almehrej, Leo Freitas, Paolo Modesti
10:00 Verifying System-level Security of a Smart Ballot Box Dana Dghaym, Thai Son Hoang, Michael Butler, Runshan Hu, Leonardo Aniello, Vladimiro Sassone
Coffee Break
10:30 - 11:00 / wonder.me
Session 2 Régine Laleau
11:00 - 12:30 / zoom
11:00 Analysing ProB’s Constraint Solving Backends Jannik Dunkelau, Joshua Schmidt, Michael Leuschel
11:30 Programming the CLEARSY Safety Platform with B Thierry Lecomte
12:00 Verifying SGAC Access Control Policies: a Comparison of ProB, Alloy and Z3 Diego de Azevedo Oliveira, Marc Frappier
12:15 ProB and Jupyter for Logic, Set Theory, Theoretical Computer Science and Formal Methods David Geleßus, Michael Leuschel
Lunch
12:30 - 13:30 / wonder.me
Keynote 1 Jonathan Bowen
13:30 - 15:30 / zoom
13:30 Modelling and Verification of Robotic Platforms for Simulation using RoboStar Technology Ana Cavalcanti
14:30 Diverse scenario exploration in model finders using graph kernels and clustering Robert Clarisó, Jordi Cabot
15:00 Sterling: A Web-based Visualizer for Relational Modeling Languages Tristan Dyer, John Baugh
15:15 VisB: A Lightweight Tool to Visualize Formal Models with SVG Graphics Michelle Werth, Michael Leuschel
Coffee Break
15:30 - 16:00 / wonder.me
Session 3 Michael Leuschel
16:00 - 17:30 / zoom
16:00 Integration of iUML-B and UPPAAL Timed Automata for Development of Real-Time Systems with Concurrent Processes Fatima Shokri-Manninen, Leonidas Tsiopoulos, Jüri Vain, Marina Waldén
16:30 Experiences on Teaching Alloy with an Automated Assessment Platform Nuno Macedo, Alcino Cunha, José Pereira, Renato Carvalho, Ricardo Silva, Ana C. R. Paiva, Miguel Sozinho Ramalho, Daniel Silva
17:00 Exploring the concept of Abstract State Machines for the runtime enforcement of software systems Elvinia Riccobene, Patrizia Scandurra
17:15 Extensible Record Structures in Event-B Asieh Salehi Fathabadi, Colin Snook, Thai Son Hoang, Dana Dghaym, Michael Butler
GMT+2
8:30
10:50
11:20
12:20
13:30
15:30
16:00
17:00
18:00
Case Study Alexander Raschke
08:30 - 10:50 / zoom
8:30 Introduction to the case study Frank Houdek
8:45 Modelling an automotive software-intensive system with adaptive features using Asmeta Paolo Arcaini, Silvia Bonfanti, Angelo Gargantini, Elvinia Riccobene, Patrizia Scandurra
9:10 Validating Multiple Variants of an Automotive Light System with Electrum Alcino Cunha, Nuno Macedo, Chong Liu
9:35 Modelling and Validating an Automotive System in Classical B and Event-B Michael Leuschel, Mareike Mutz, Michelle Werth
10:00 An Event-B Model of an Automotive Adaptive Exterior Light System Amel Mammar, Marc Frappier, Regine Laleau
10:25 A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System Sebastian Krings, Philipp Koerner, Jannik Dunkelau, Chris Rutenkolk
Coffee Break
10:50 - 11:20 / wonder.me
Session 4 Patrizia Scandurra
11:20 - 12:20 / zoom
11:20 Formalizing and Analyzing System Requirements of Automatic Train Operation over ETCS using Event-B Robert Eschbach
11:35 Automatic Transformation of SysML Model to Event-B Model for Railway CCS application Shubhangi Salunkhe, Randolf Berglehner, Abdul Rasheeq
11:50 Formal distributed protocol development for reservation of railway sections Paulius Stankaitis, Alexei Iliasov, Tsutomu Kobayashi, Yamine Ait-Ameur, Alexander Romanovsky, Fuyuki Ishikawa
Lunch
12:20 - 13:30 / wonder.me
Keynote 2 Dominique Méry
13:30 - 15:30 / zoom
13:30 Sharing proofs across logics and systems: a boost for formal methods? Gilles Dowek
14:30 Validation of Formal Models by Timed Probabilistic Simulation Fabian Vu, Michael Leuschel, Atif Mashkoor
15:00 Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B Héctor Ruíz Barradas, Lilian Burdy, David Deharbe
15:15 Refinement and Verification of Responsive Control Systems Karla Morris, Colin Snook, Thai Son Hoang, Geoffrey Hulette, Robert Armstrong, Michael Butler
Coffee Break
15:30 - 16:00 / wonder.me
Session 5 Elvinia Riccobene
16:00 - 17:00 / zoom
16:00 The CamilleX Framework for the Rodin Platform Thai Son Hoang, Colin Snook, Dana Dghaym, Asieh Salehi Fathabadi, Michael Butler
16:15 Structuring the State and Behavior of ASMs: Introducing a Trait-Based Construct for Abstract State Machine Languages Philipp Paulweber, Emmanuel Pescosta, Uwe Zdun
16:30 About the Concolic Execution and Symbolic ASM Function Promotion in CASM Philipp Paulweber, Jakob Moosbrugger, Uwe Zdun
16:45 Towards a Shared Specification Repository Philipp Koerner, Michael Leuschel, Jannik Dunkelau
Steering Committee Meeting
17:00 - 18:00 / zoom
GMT+2
08:30
10:45
11:15
12:30
13:15
15:30
15:45
16:00
17:30
PhD Symposium Yamine Ait-Ameur
08:30 - 10:45 / zoom
8:30 A Correct by Construction Approach for the Modeling and the Verification of Cyber-Physical Systems in Event-B Meryem Afendi
8:45 Automatic Generation of DistAlgo Programs from Event-B Models Alexis Grall
9:00 A Formal Approach for the Modeling of High-Level Architectures Aligned with System Requirements Racem Bougacha
9:15 Event-B: From Systems to Sub-systems Modeling Kenza Kraibi
9:30 Formal Meta Engineering Event-B: Extension and Reasoning The EB4EB Framework Peter Riviere
9:45 Formalizing the Institution for Event-B in the Coq Proof Assistant Conor Reynolds
10:00 Improving the Trustworthiness of Self-driving Systems. Fahad Alotaibi
10:15 A Framework for Critical Interactive SystemFormal Modelling and Analysis Ismail Mendil
10:30 A modeling and verification framework for security protocols Mario Lilli
Coffee Break
10:45 - 11:15 / wonder.me
Session 6 Gerhard Schellhorn
11:15 - 12:30 / zoom
11:15 A Logic for Reflective ASMs Klaus-Dieter Schewe, Flavio Ferrarotti
11:45 Towards Refinement of Unbounded Parallelism in ASMs Using Concurrency and Reflection Fengqing Jiang, Neng Xiong, Xinyu Lian, Senén González, Klaus-Dieter Schewe
12:00 Partial-order distributed ASM runs and recursion: The Foundational Context Egon Börger, Klaus-Dieter Schewe
Lunch
12:30 - 13:15 / wonder.me
Session 7 Colin Snook
13:15 - 15:30 / zoom
13:15 Unbounded Barrier-Synchronized Concurrent ASMs for Effective MapReduce Processing on Streams Zilinghan Li, Shilan He, Yiqing Du, Senén González, Klaus-Dieter Schewe
13:45 Adding Concurrency to a Sequential Refinement Tower Gerhard Schellhorn, Stefan Bodenmüller, Jörg Pfähler, Wolfgang Reif
14:15 Event-B formalization of Event-B contexts Jean-Paul Bodeveix, Mamoun Filali-Amine
14:45 Extending ASMETA with time features Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini, Elvinia Riccobene
15:00 Modelling Hybrid Programs with Event-B Meryem Afendi, Régine Laleau, Amel Mammar
Presentation of new case study for ABZ 2023 (Nancy)
15:30 - 15:45 / zoom
Coffee Break
15:45 - 16:00 / wonder.me
Session 8 Marc Frappier
16:00 - 17:30 / zoom
16:00 Formally Verified Architecture Patterns of Hybrid Systems Using Proof and Refinement with Event-B Guillaume Dupont, Yamine Ait Ameur, Marc Pantel, Neeraj Singh
16:30 Event-B-Supported Choreography-Defined Communicating Systems: Correctness and Completeness Yamine Ait Ameur, Sarah Benyagoub, Klaus-Dieter Schewe
17:00 Formal Verification of Interoperability between Future Network Architectures using Alloy Mohammad Jahanian, Jiachen Chen, K. K. Ramakrishnan
Farewell Alexander Raschke
17:30 / zoom