The ABZ conference series is dedicated to the cross-fertilization of state-based and machine-based formal methods. The naming “ABZ” has historical reasons and is not meant to favor any methods. On the contrary, any state-based or even hybrid formal method is welcome in the ABZ community!

The following enumeration is just an excerpt of the methods from which research results have been published on ABZ. The methods Abstract State Machines (ASM), Alloy, Classical B, Event-B, Temporal Logic of Actions (TLA), Vienna Development Method (VDM), Z Notation, and much more share a common conceptual foundation and are widely used in both academia and industry for the design and analysis of hardware and software systems.

This conference aims for a vital exchange of knowledge and experience among the research communities around these different formal methods.

This website is now intended to provide a central entry point into the ABZ community around the ABZ conference. Like the conference, we want to bring together on a single page the various rigorous state-based methods that form the core of the ABZ community and provide an overview for interested researchers.

In addition to listing all past and upcoming events, it briefly describes some methods themselves and, where available, links to specific websites that provide more details about these exemplary state-based formal methods. The database of all papers published in connection with ABZ provides a deeper insight into past and current research in this area.

A session dedicated to a shared real-life case study among all the methods is included since ABZ 2014. The objective of this session was to enrich the set of case studies developed with ABZ methods with a practical and real-life case study. Here, we provide a detailed description of these case studies and the corresponding publications. The publications section provides the archived models, applied formal approaches, resources, and tools created or used in the context of the case studies.

Upcoming Conference

Past & Upcoming Editions

ABZ 2024 (Bergamo, Italy)

10th International Conference on Rigorous State-Based Methods

ABZ 2023 (Nancy, France)

9th International Conference on Rigorous State-Based Methods

ABZ 2021 (Ulm, Germany)

8th International Conference on Rigorous State-Based Methods

Case Studies

Mechanical Lung Ventilator (ABZ 2024)

This document presents the case study for ABZ 2024 conference. The case study introduces Mechanical Lung Ventilator (MLV). The MLV is intended to provide ventilation support for patients that require mechanical ventilation in two operative modes: Pressure Controlled Ventilation (PCV) and Pressure Support Ventilation (PSV).

AMAN Case Study (ABZ 2023)

This document presents the case study for ABZ 2023 conference. The case study introduces a safety critical interactive system called AMAN (Arrival MANager) which is a partly-autonomous scheduler of landing sequences of aircraft in airports.

Adaptive Exterior Light and Speed Control System (ABZ 2020)

This document describes two systems from the automotive domain: an adaptive exterior light system (ELS) and a speed control system (SCS). This specification is based on the SPES XT running example.