ABZ 2026, Program

ABZ 2026, Program

You're viewing the program in a time zone which is different from your device's time zone change time zone

Mon 18 May
Displayed time zone: Osaka, Sapporo, Tokyo change

	18:15 - 19:15	ABZ Gedenkschrift for Jean-Raymond AbrialABZ at 2F Conf Room 2 Chair(s): Yamine Ait Ameur IRIT/INPT-ENSEEIHT

	18:15 60m Talk		Gedenkschrift for Jean-Raymond AbrialABZ

Tue 19 May
Displayed time zone: Osaka, Sapporo, Tokyo change

	08:30 - 09:00	RegistrationServices at Registration Area / Entrance

	08:30 30m Registration		Registration

	09:00 - 09:10	ABZ OpeningABZ at 2F Conf Room 4

	09:00 10m Talk		ABZ Opening

	09:10 - 10:10	ABZ Invited Talk 1: Toshiaki AokiABZ at 2F Conf Room 4

	09:10 60m Keynote		Practical Applications of Formal Methods to Automotive Systems: From In-Vehicle Systems to Autonomous Driving Toshiaki Aoki JAIST

	10:10 - 10:35	ABZ Session 1: Concurrent and Distributed SystemsABZ at 2F Conf Room 4 Chair(s): Dominique Mery Université de Lorraine, CNRS, INRIA / LORIA & Telecom Nancy, France

	10:10 25m Talk		A Method for Testing Partial-Order Reduction Theories in Alloy Mara Miulescu Eindhoven University of Technology, Thomas Neele Eindhoven University of Technology

	10:30 - 11:00	BreakServices at 2F Common Area / Each Workshop/Tutorial Room

	10:30 30m Coffee break		Break

	11:00 - 12:30	ABZ Session 1: Concurrent and Distributed SystemsABZ at 2F Conf Room 4 Chair(s): Dominique Mery Université de Lorraine, CNRS, INRIA / LORIA & Telecom Nancy, France

	11:00 25m Talk		Identifying Design Flaws in a Lock-Free Task Pool with TLA+ Ilya Shchepetkov Kaspersky Lab, Vasil Dyadov Kaspersky Lab, Alexander Kogtenkov Kaspersky Lab
	11:25 25m Talk		Formal Modelling and Analysis of the ORAN O2 Interface in Alloy: Implications for NTN Deployment Sean McLaren University of Glasgow, Tsutomu Kobayashi Japan Aerospace Exploration Agency (JAXA), Leon Wong Rakuten Mobile, Inc, Paul Harvey Rakuten Mobile Innovation Studio
	11:50 25m Talk		Formal Verification of Healthcare Computer Network Architectures using Alloy and TLA+ Daniel Daukševič Institute of Computer Science, Vilnius University, Vilnius,Lithuania, Linas Laibinis Institute of Computer Science, Vilnius University, Vilnius,Lithuania
	12:15 15m Talk		Formal Verification of Decentralized Autonomous Organizations Simone Valentini University of Milan, Sowelu Avanzo University of Turin, Elvinia Riccobene Computer Science Dept., University of Milan

	12:30 - 14:00	LunchServices at 2F Common Area / Each Workshop/Tutorial Room

	12:30 90m Lunch		Lunch

	13:45 - 14:45	ABZ Invited Talk 2: Jin Song DongABZ at 2F Conf Room 4

	13:45 60m Keynote		Reasoning Beyond LLM: Formal Methods Agents Jin Song Dong National University of Singapore

	14:45 - 15:50	ABZ Session 2: Safety and SecurityABZ at 2F Conf Room 4 Chair(s): Marc Frappier Université de Sherbrooke, Canada

	14:45 25m Talk		Relational Verification of Identity Disclosure Using Alloy Seungil Yang Japan Advanced Institute of Science and Technology (JAIST), Peter Riviere Japan Advanced Institute of Science and Technology (JAIST), Toshiaki Aoki JAIST
	15:10 25m Talk		Security-Minded Modelling and Verification of Autonomous Satellite Docking Juel Hussain University of Manchester, Marie Farrell The University of Manchester, Louise Dennis University of Manchester, Clare Dixon University of Manchester
	15:35 15m Talk		SHARCS: Refinement-Centric Hazard Analysis of Requirements for Critical Systems Asieh Salehi Fathabadi University of Southampton, Thai Son Hoang University of Southampton, Michael Butler University of Southampton

	15:30 - 16:00	BreakServices at 2F Common Area / Each Workshop/Tutorial Room

	15:30 30m Coffee break		Break

	16:15 - 17:20	ABZ Session 3: Methods (1)ABZ at 2F Conf Room 4 Chair(s): Maurice ter Beek CNR-ISTI Pisa, Italy

	16:15 25m Talk		Slicing Models for Equiconsistency with Alloy Marc Thieme Karlsruhe Institute of Technology, Shobhit Singh Karlsruhe Institute of Technology, Terru Stübinger Karlsruhe Institut für Technologie, Romain Pascual MICS, CentraleSupélec, Université Paris-Saclay, Mattias Ulbrich KIT
	16:40 25m Talk		Verifying Properties of State-Based Models using Constraint Programming Victoria Johnson University of Sheffield, Pedro Ribeiro University of York, UK, Simon Foster University of York, Peter Nightingale University of York, Felix Ulrich-Oltean University of York
	17:05 15m Talk		Why does it fail? Explanation of verification failures Lars-Henrik Eriksson Uppsala University

	17:35 - 18:40	ABZ Session 4: AutonomyABZ at 2F Conf Room 4 Chair(s): Regine Laleau Paris Est Creteil University

	17:35 25m Talk		Encoding BDI Syntax with Theories in Event-B Mengwei Xu University of Newcastle, Peter Riviere Japan Advanced Institute of Science and Technology (JAIST), Toshiaki Aoki JAIST, Marie Farrell The University of Manchester, Yamine Ait Ameur IRIT/INPT-ENSEEIHT, Neeraj Singh INPT-ENSEEIHT / IRIT, University of Toulouse, France, Guillaume Dupont INPT–ENSEEIHT
	18:00 25m Talk		Fuzzing executable ASMETA models Gabriele Bellini University of Milan, Elvinia Riccobene Computer Science Dept., University of Milan
	18:25 15m Talk		Human-Centred Formal Verification: A Vision for Bridging Technical Rigour with Stakeholder Needs in Autonomous Systems Asieh Salehi Fathabadi University of Southampton, Sebastian Stein University of Southampton

	18:45 - 20:15	ABZ Welcome ReceptionABZ at 2F Break/Lunch Room

	18:45 90m Dinner		ABZ Welcome Reception

Wed 20 May
Displayed time zone: Osaka, Sapporo, Tokyo change

	08:30 - 09:00	RegistrationServices at Registration Area / Entrance

	08:30 30m Registration		Registration

	09:00 - 09:15	FM OpeningMain Plenaries / Invited Talks at 2F Auditorium

	09:00 15m Talk		FM 2026 Opening

	09:15 - 10:25	FM/ABZ Keynote: Ichiro HasuoMain Plenaries / Invited Talks at 2F Auditorium

	09:15 70m Keynote		Cutting out FM Angles from the Jungle of Automated Driving Ichiro Hasuo National Institute of Informatics, Japan

	10:25 - 10:45	FME Lucas AwardMain Plenaries / Invited Talks at 2F Auditorium

	10:45 - 11:15	BreakServices at 2F Break/Lunch Room

	10:45 30m Coffee break		Break

	11:15 - 12:15	ABZ Invited Talk 3: Dominique MeryABZ at 1F Room 101-103

	11:15 60m Keynote		Systematic Development of Distributed Algorithms using Event-B - Experiences, reviews and prospects - Dominique Mery Université de Lorraine, CNRS, INRIA / LORIA & Telecom Nancy, France

	12:15 - 12:30	ABZ Overview of Gedenkschrift for Jean-Raymond AbrialABZ at 1F Room 101-103

	12:15 15m Talk		Overview of Gedenkschrift for Jean-Raymond Abrial

	12:30 - 13:50	LunchServices at 2F Break/Lunch Room

	12:30 80m Lunch		Lunch

	13:50 - 15:00	FM Industry Keynote: Daniel KroeningMain Plenaries / Invited Talks at 2F Auditorium

	13:50 70m Keynote		The Industrial Perspective on GenAI for Formal Methods Daniel Kroening Amazon

	15:00 - 15:30	BreakServices at 2F Break/Lunch Room

	15:00 30m Coffee break		Break

	15:30 - 16:35	ABZ Session 5: Methods (2)ABZ at 1F Room 101-103 Chair(s): Asieh Salehi Fathabadi University of Southampton

	15:30 25m Talk		Counterexample-Guided Interval Weakening Ben M. Andrew University of Manchester, Marie Farrell The University of Manchester, Louise Dennis University of Manchester, Michael Fisher University of Manchester, UK
	15:55 25m Talk		Specification and Analysis of Ethical Requirements in Autonomous Systems using Abstract State Machines Patrizia Scandurra University of Bergamo, Italy, Martina De Sanctis Gran Sasso Science Institute, Gianluca Filippone Gran Sasso Science Institute, L'Aquila, Italy, Paola Inverardi Gran Sasso Science Institute, Raffaela Mirandola Karlsruhe Institute of Technology (KIT), Sara Pettinari Gran Sasso Science Institute
	16:20 15m Talk		Evaluating the Practical Impact of Parallelism in Asmeta Andrea Bombarda University of Bergamo, Silvia Bonfanti University of Bergamo, Cesar Cornejo University of Bergamo, Angelo Gargantini University of Bergamo, Nico Pellegrinelli University of Bergamo

	16:35 - 16:50	Short BreakServices at 2F Break/Lunch Room

	16:35 15m Coffee break		Break

	16:45 - 18:00	ABZ Session 6: Case StudyABZ at 1F Room 101-103 Chair(s): Marie Farrell The University of Manchester, Tsutomu Kobayashi Japan Aerospace Exploration Agency (JAXA)

	16:45 25m Talk		Formal Modeling and Analysis of a Planetary Rover under Abnormal Scenarios with Quint Riki Nakamura The University of Tokyo, Shunichiro Nomura The University of Tokyo, Takahiro Kato The University of Tokyo, Takato Hatae The University of Tokyo, Satoshi Ikari The University of Tokyo, Ryu Funase The University of Tokyo, Shinichi Nakasuka The University of Tokyo
	17:10 25m Talk		Can Large Language Models Support Modeling Systems with ASMETA? A Case Study with a Planetary Rover Andrea Bombarda University of Bergamo, Silvia Bonfanti University of Bergamo, Angelo Gargantini University of Bergamo, Nico Pellegrinelli University of Bergamo
	17:35 25m Talk		A Spectabular Model of an Automotive Adaptive Exterior Light System Emil Sekerinski McMaster University, Canada

	18:00 - 18:10	ABZ Award and ClosingABZ at 1F Room 101-103

	18:00 10m Talk		ABZ Award and Closing

	18:10 - 18:30	Walk to Reception at TKPMain Plenaries / Invited Talks at Reception Venue: TKP Garden City PREMIUM Jinbocho

	18:10 20m Dinner		Move to Reception

	18:30 - 20:30	ReceptionMain Plenaries / Invited Talks at Reception Venue: TKP Garden City PREMIUM Jinbocho

	18:30 2h Dinner		Reception

Comments