ABZ 2026, Program


Plenary
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 Abrial
Tue 19 May
    
08:30
30m
Registration

09:00 - 09:10
    
ABZ Opening ABZ at 2F Conf Room 4
    
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

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
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
Talk
Identifying Design Flaws in a Lock-Free Task Pool with TLA+
Ilya Shchepetkov Kaspersky Lab, Vasil Dyadov Kaspersky Lab, Alexander Kogtenkov Kaspersky Lab

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

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

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    
13:45 - 14:45
    
ABZ Invited Talk 2: Jin Song DongABZ at 2F Conf Room 
Keynote
Reasoning Beyond LLM: Formal Methods Agents
Jin Song Dong National University of Singapore

ABZ Session 2: Safety and SecurityABZ at 2F Conf Room 4

Chair(s): Marc Frappier Université de Sherbrooke, Canada
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

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

Salehi Fathabadi University of Southampton, Thai Son Hoang University of Southampton, Michael Butler University of Southampton

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

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

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

Why does it fail? Explanation of verification failures
Lars-Henrik Eriksson Uppsala University

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

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

Fuzzing executable ASMETA models
Gabriele Bellini University of Milan, Elvinia Riccobene Computer Science Dept., University of Milan

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


    
FM OpeningMain Plenaries / Invited Talks at 2F Auditorium

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

Keynote
    
Cutting out FM Angles from the Jungle of Automated Driving
Ichiro Hasuo National Institute of Informatics, Japan

FME Lucas AwardMain Plenaries / Invited Talks at 2F Auditorium


ABZ Invited Talk 3: Dominique Mery ABZ at 1F Room 101-103

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

ABZ Overview of Gedenkschrift for Jean-Raymond AbrialABZ at 1F Room 101-103

Overview of Gedenkschrift for Jean-Raymond Abrial

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

Keynote
    
The Industrial Perspective on GenAI for Formal Methods
Daniel Kroening Amazon

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


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

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

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

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


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)

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

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

A Spectabular Model of an Automotive Adaptive Exterior Light System
Emil Sekerinski McMaster University, Canada

ABZ Award and ClosingABZ at 1F Room 101-103

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


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
Organizing Committee

    Fuyuki Ishikawa
    Fuyuki IshikawaGeneral Co-Chair
    National Institute of Informatics
    Japan
    Alcino Cunha
    Alcino CunhaGeneral Co-Chair
    University of Minho; INESC TEC
    Portugal
    Marie Farrell
    Marie FarrellCase Study Track Co-Chair
    The University of Manchester
    United Kingdom
    Tsutomu Kobayashi
    Tsutomu KobayashiCase Study Track Co-Chair
    Japan Aerospace Exploration Agency (JAXA)
    Japan

Comments

Post a Comment

Popular posts from this blog

Jean-Raymond Abrial (1938, 2025)

Image
  Jean-Raymond Abrial (1938, 2025) Jean-Raymond Abrial est décédé les 26 mai 2025 la vieille de la conférence qui a eu lieu dans le cadre des Journées Scientifiques de l'université de Nantes et qui traitait de ses travaux et de leur mise en oeuvre dans différentes domaines.J.-R Abrial est né en 1938 à Versailles. Après des études au Prytanée militaire de la Flèche, il fera l'Ecole Polytechnique. En 1960 il sera ingénieur du génie maritime. Il sera boursier du gouvernement français à Stanford University puis au Centre de Programmation de la Marine où il travaillera sur une version du langage LTR (Langage Temps Réel). C'est là que Gérard Le Lann, qui a fait partie de l'équipe ayant conçu Internet, l'a connu. J.-R Abrial est pour lui "l'un des plus grands informaticiens français ! Peu enclin à épouser les « modes » qui agitent plus ou moins régulièrement les communautés scientifiques. Liberté de penser, de créer, et liberté d'essaimer !".A Grenoble, d...
Read more

Ce que je dois à Jean-Raymond Abrial

Image
 Quand ai-je découvert Jean-Raymond Abrial ?  Peut-être bien que c'est quand j'ai fait acheter les actes de la conférence de Cargèse et que j'ai lu son article Data Semantics . Ou est-ce lors de la lecture des publications de la DER-IMA d'EDF (située à Clamart) ? Ce qui est sûr c'est que j'ai découvert Z dans le Meyer Baudoin, Méthodes de Programmation chez Eyrolles, puis dans le Delobel Adiba, Bases de données chez Dunod. Quand j'ai débuté en "informatique de gestion" (en I.U.T "Informatique") je trouvais que ce que je lisais était bien peu "scientifique". "Information" "donnée" "rubrique" etc.  Pour "donnée" j'ai appris les théorèmes de Jean-Louis Rigal qui était prof à l'Université Dauphine. Facile : Th1, "Une donnée n'est pas donnée" car c'est le résultat d'une abstraction, Th 2. "Une donnée n'est pas donnée" car une fois donnée, ce n'est...
Read more

" Aurica.ai can make mistakes. Check important info."

 On trouve des choses étonnantes sur la Toile. Je ne devrais pas m'étonner. J'ai bien enregistré un document où j'appelle Papygram ce qui est un diagramme sagittal ou arrow diagram ou mapping diagram . J'avais fait confiance à un collègue professeur de maths qui m'avait nommé ainsi ces diagrammes. Et j'avais plaisir à faire connaître monsieur et madame Papy, mathématiciens belges sur lesquels Dieudonné avait écrit. Le papygram ce ne sont pas deux patates avec des flèches allant de l'une à l'autre, mais une grosse patate avec des éléments dans la patate qui sont reliés par des flèches. C'est une autre représentation des relations.  Cette correction étant faite, revenons à notre découverte.  Voici ce que je viens de trouver. Le texte est un bel hommage à Jean-Raymond Abrial. Mais l'auteur parle de Jean-Marie Charles Abrial. Je comprends pourquoi il arrive que les "IA" nous étonnent. Notez que sur la page que je colle ci-dessous, dans une...
Read more