Heterogeneous Specification via Institutions for Event-B and Temporal Logic (WADT 2026) - WADT 2026

Tue 30 Jun 2026

co-located with STAF 2026

Who

Richard Flynn, Marie Farrell, Rosemary Monahan, James Power, Michael Fisher

Track

Time Zone

The program is currently displayed in (GMT+02:00) Brussels, Copenhagen, Madrid, Paris.

Use conference time zone: (GMT+02:00) Brussels, Copenhagen, Madrid, ParisSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

Tue 30 Jun 2026 14:10 - 14:30 at Turing - Session 2

Abstract

This work explores the use of Institution Theory as an approach for combining the formal methods tool Event-B with Temporal Logic systems. We define an institution for Linear-Time Temporal Logic and uses this to demonstrate temporal properties for Event-B through a duplex institution EVT+LTL.

Richard Flynn

Maynooth University

Marie Farrell

The University of Manchester

United Kingdom

Rosemary Monahan

Ireland

James Power

Maynooth University

Ireland

Michael Fisher

University of Manchester, UK

United Kingdom

Time Zone

The program is currently displayed in (GMT+02:00) Brussels, Copenhagen, Madrid, Paris.

Use conference time zone: (GMT+02:00) Brussels, Copenhagen, Madrid, ParisSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

Tue 30 Jun
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

	13:30 - 15:00	Session 2WADT 2026 at Turing Session Chair: Alexandre Madeira

	13:30 20m Talk		Algebraic Specification of Card-Based Cryptographic Protocols in Rocq WADT 2026 Cheng-Hui Weng Nagoya University
	13:50 20m Talk		Weighted Attribute Grammars: Reconciling Weighted and Attribute Grammars WADT 2026 Marcus Gerhold University of Twente, The Netherlands, Vadim Zaytsev University of Twente Pre-print
	14:10 20m Talk		Heterogeneous Specification via Institutions for Event-B and Temporal Logic WADT 2026 Richard Flynn Maynooth University, Marie Farrell The University of Manchester, Rosemary Monahan , James Power Maynooth University, Michael Fisher University of Manchester, UK
	14:30 20m Talk		Temporal Predicate Transformers: A Preliminary Study WADT 2026 Ānrán Wáng Saarland University, Lena Verscht Saarland University; RWTH Aachen University; , Benjamin Lucien Kaminski Saarland University; University College London