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:
- Regular research paper: 20min presentation + 10min discussion
- Case study contribution: 15min presentation + 10min discussion
- Short paper and PhD symposium: 10min presentation + 5min discussion
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
9:20
Some Thoughts on Computational Models: From Massive Human Computing to Abstract State Machines, and Beyond
9:40
Some Observations on Mitotic Sets
10:00
Communities and Ancestors Associated with Egon Börger and ASM
10:20
Models and Modelling in Computer Science
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
11:50
Flashix: Modular Verification of a Concurrent and Crash-Safe Flash File System
12:10
The ASMETA Approach to Safety Assurance of Software Systems
12:30
Spot the Difference: A Detailed Comparison Between B and Event-B
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
14:20
Language and Communication Problems in Formalization: a Natural Language Approach
14:40
Moded and Continuous Abstract State Machines
15:00
What is the Natural Abstraction Level of an Algorithm?
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
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
16:40
ASM Specification and Refinement of a Quantum Algorithm
17:00
Analysis of Mobile Networks' Protocols Based on Abstract State Machines
17:20
A Stepwise Design Optimization Problem
17:40
Computation on Structures: Behavioural Theory, Logic, Complexity
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
9:30
OntoEventB: A Generator of Event-B contexts from Ontologies
9:50
EVBT — an Event-B tool for code generation and documentation
10:10
Scenario Checker: An Event-B tool for validating abstract models
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
11:30
Examples of using the Instantiation Plug-in
11:50
Data-types definitions: Use of Theory and Context instantiations Plugins
12:10
Towards CamilleX 3.0
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
14:20
Large Scale Biological Models in Rodin
14:40
Formal Verification of EULYNX Models Using Event-B and RODIN
Coffee Break
15:00 - 15:30
/
wonder.me
15:30 - 17:30
/
demio
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
8:45
Towards ASM-based automated formal verification of security protocols
9:15
Proving the safety of a Sliding Window Protocol with Event B
9:45
Account and Transaction Protocol of the Open Banking Standard
10:00
Verifying System-level Security of a Smart Ballot Box
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
11:30
Programming the CLEARSY Safety Platform with B
12:00
Verifying SGAC Access Control Policies: a Comparison of ProB, Alloy and Z3
12:15
ProB and Jupyter for Logic, Set Theory, Theoretical Computer Science and Formal Methods
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
14:30
Diverse scenario exploration in model finders using graph kernels and clustering
15:00
Sterling: A Web-based Visualizer for Relational Modeling Languages
15:15
VisB: A Lightweight Tool to Visualize Formal Models with SVG Graphics
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
16:30
Experiences on Teaching Alloy with an Automated Assessment Platform
17:00
Exploring the concept of Abstract State Machines for the runtime enforcement of software systems
17:15
Extensible Record Structures in Event-B
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
8:45
Modelling an automotive software-intensive system with adaptive features using Asmeta
9:10
Validating Multiple Variants of an Automotive Light System with Electrum
9:35
Modelling and Validating an Automotive System in Classical B and Event-B
10:00
An Event-B Model of an Automotive Adaptive Exterior Light System
10:25
A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System
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
11:35
Automatic Transformation of SysML Model to Event-B Model for Railway CCS application
11:50
Formal distributed protocol development for reservation of railway sections
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?
14:30
Validation of Formal Models by Timed Probabilistic Simulation
15:00
Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B
15:15
Refinement and Verification of Responsive Control Systems
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
16:15
Structuring the State and Behavior of ASMs: Introducing a Trait-Based Construct for Abstract State Machine Languages
16:30
About the Concolic Execution and Symbolic ASM Function Promotion in CASM
16:45
Towards a Shared Specification Repository
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
8:45
Automatic Generation of DistAlgo Programs from Event-B Models
9:00
A Formal Approach for the Modeling of High-Level Architectures Aligned with System Requirements
9:15
Event-B: From Systems to Sub-systems Modeling
9:30
Formal Meta Engineering Event-B: Extension and Reasoning The EB4EB Framework
9:45
Formalizing the Institution for Event-B in the Coq Proof Assistant
10:00
Improving the Trustworthiness of Self-driving Systems.
10:15
A Framework for Critical Interactive SystemFormal Modelling and Analysis
10:30
A modeling and verification framework for security protocols
Coffee Break
10:45 - 11:15
/
wonder.me
Session 6 Gerhard Schellhorn
11:15 - 12:30
/
zoom
11:15
A Logic for Reflective ASMs
11:45
Towards Refinement of Unbounded Parallelism in ASMs Using Concurrency and Reflection
12:00
Partial-order distributed ASM runs and recursion: The Foundational Context
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
13:45
Adding Concurrency to a Sequential Refinement Tower
14:15
Event-B formalization of Event-B contexts
14:45
Extending ASMETA with time features
15:00
Modelling Hybrid Programs with Event-B
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
16:30
Event-B-Supported Choreography-Defined Communicating Systems: Correctness and Completeness
17:00
Formal Verification of Interoperability between Future Network Architectures using Alloy
ABZ2021 on Twitter