2F Auditorium - FM 2026

VenueHitotsubashi Hall

Room name2F Auditorium

Floor2

Room InformationNo extra information available

Program

Time Zone

The program is currently displayed in (GMT+09:00) Osaka, Sapporo, Tokyo.

Use conference time zone: (GMT+09:00) Osaka, Sapporo, TokyoSelect 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

Save

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

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

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

09:00 15m Talk		FM 2026 Opening Main Plenaries / Invited Talks Augusto Sampaio Universidade Federal de Pernambuco, Marielle Stoelinga University of Twente and Radboud University, Nijmegen, Fuyuki Ishikawa National Institute of Informatics

09:15 - 10:25	FM/ABZ Keynote: Ichiro HasuoMain Plenaries / Invited Talks at 2F Auditorium Chair(s): Marielle Stoelinga University of Twente and Radboud University, Nijmegen

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

	10:25 - 10:45	FME Lucas AwardMain Plenaries / Invited Talks at 2F Auditorium Chair(s): Ana Cavalcanti University of York

11:15 - 12:30	Session 1: Information Flow VerificationResearch Track at 2F Auditorium Chair(s): Graeme Smith The University of Queensland

11:15 25m Talk		Differential Verification of Information Flow in SEAndroid Policies Research Track Lorenzo Ceragioli IMT Lucca, Italy, Letterio Galletta IMT School for Advanced Studies Lucca, Edoardo Lunati IMT School for Advanced Studies Lucca
11:40 25m Talk		History-Constrained Systems Research Track Louwe B. Kuijer University of Liverpool, David Purser University of Liverpool, Henry Sinclair-Banks University of Warsaw, Patrick Totzke University of Liverpool
12:05 25m Talk		FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines Research Track Xindi Zhang Institute of Software / CAS China, Furong Ye LIACS, Leiden University, Zhihan Chen Institute of Software, Chinese Academy of Sciences, Shaowei Cai Institute of Software at Chinese Academy of Sciences

13:50 - 15:00	FM Industry Keynote: Daniel KroeningMain Plenaries / Invited Talks at 2F Auditorium Chair(s): Augusto Sampaio Universidade Federal de Pernambuco

13:50 70m Keynote		The Industrial Perspective on GenAI for Formal Methods Main Plenaries / Invited Talks Daniel Kroening Amazon

15:30 - 16:25	Journal-FirstJournal First at 2F Auditorium

15:30 5m Talk		Journal-First Opening Talk Journal First
15:35 25m Talk		Modelling and Analysing Routing Protocols Diagrammatically with Bigraphs Journal First Michele Sevegnani University of Glasgow Link to publication
16:00 25m Talk		Memory Consistency and Program Transformations Journal First Akshay Gopalakrishnan McGill University Link to publication

16:50 - 18:05	TAP Session 1: Formal Languages, Reachability, and Program VerificationTAP Track at 2F Auditorium Chair(s): Bernhard Aichernig Johannes Kepler University Linz

16:50 25m Talk		Correct-by-Construction Dynamic Reachability: A Galois-Connected Approach to Bidirected Dyck Languages TAP Track Xiaofei Zhao Lanzhou Petrochemical University of Vocational Technology DOI
17:15 25m Talk		EUF-based Solving Dyck-Reachability with Applications to Static Analysis TAP Track Yide Du College of Computer Science and Technology, NationalUniversity of Defense Technology, Zhenbang Chen College of Computer, National University of Defense Technology, Kunlin Liu School of Computer, National University of Defense Technology, China, Guofeng Zhang College of Computer, National University of Defense Technology, Xudong Wang College of Computer Science and Technology, NationalUniversity of Defense Technology, Ke Ma , Wei Dong National University of Defense Technology, Ji Wang National University of Defense Technology
17:40 25m Talk		Towards Formally Verified Smart Contracts Compilation TAP Track Elvira Albert , Samir Genaim Universidad Complutense de Madrid, Enrique Martin-Martin Universidad Complutense de Madrid

Thu 21 May
Displayed time zone: Osaka, Sapporo, Tokyo change

09:00 - 10:10	FM/TAP Keynote: Cristian CadarMain Plenaries / Invited Talks at 2F Auditorium Chair(s): Nikolai Kosmatov Thales Research & Technology

09:00 70m Keynote		Testing and Analysis in the AI Era Main Plenaries / Invited Talks Cristian Cadar Imperial College London

10:40 - 12:30	Session 2: Neural Networks VerificationResearch Track at 2F Auditorium Chair(s): Mark van Wijk University of Twente

10:40 25m Talk		Exact Verification of Graph Neural Networks with Incremental Constraint Solving Research Track Minghao Liu University of Oxford, Chia-Hsuan Lu University of Oxford, Marta Kwiatkowska University of Oxford
11:05 25m Talk		Formal Reasoning About Confidence and Automated Verification of Neural Networks Research Track Mohammad Afzal TCS Research Pune and IIT Bombay India, S. Akshay Indian Institute of Technology, Bombay, India, Blaise Genest IPAL - CNRS - CNRS@CREATE, Ashutosh Gupta Indian Institute of Technology Bombay
11:30 25m Talk		Mining Verdict Boundaries for Neural Network Verification Research Track Jiawei Ren University of New South Wales, Guanqin Zhang University of New South Wales, Sydney, Zhenya Zhang Kyushu University, Yulei Sui University of New South Wales
11:55 25m Talk		SAPSE-Synergy: Balancing Formal Soundness and Empirical Coverage in Neural Theorem Proving Research Track Minrui Chen Kyushu University, Huidong Jiang Institute of Science Tokyo, Hiroto Saigo Kyushu University

14:10 - 15:35	FM4All & ACM Reference CurriculumCommunity Sessions at 2F Auditorium

14:10 85m Talk		FM4All - FME Guidelines for Teaching Formal Methods as a Knowledge Area in the ACM Curriculum Community Sessions Luigia Petre Åbo Akademi University File Attached

16:05 - 17:55	Session 4: LLMs Formal MethodsResearch Track at 2F Auditorium Chair(s): Carlo A. Furia Università della Svizzera italiana (USI)

16:05 25m Talk		Can LLM Aid in Solving Constraints with Inductive Definitions? Research Track Weizhi Feng Institute of Software, Chinese Academy of Sciences, Shidong Shen Institute of Software, Chinese Academy of Sciences, Jiaxiang Liu Institute of Software, Chinese Academy of Sciences, Taolue Chen Birkbeck, University of London, Fu Song Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences; Nanjing Institute of Software Technology, Zhilin Wu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
16:30 25m Talk		Towards Language Model Guided TLA+ Proof Automation Research Track Yuhao Zhou , Stavros Tripakis Northeastern University
16:55 25m Research paper		Validating Formal Specifications with LLM-generated Test Cases Research Track Alcino Cunha University of Minho; INESC TEC, Nuno Macedo University of Porto; INESC TEC Pre-print File Attached
17:20 25m Talk		ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest and Repair Research Track Zhiyong Chen Nanjing University, Jialun Cao Hong Kong University of Science and Technology, Chang Xu Nanjing University, Shing-Chi Cheung Department of Computer Science and Engineering, The HongKong University of Science and Technology, Hong Kong, China

Fri 22 May
Displayed time zone: Osaka, Sapporo, Tokyo change

09:00 - 10:10	FM Keynote: Ruzica PiskacMain Plenaries / Invited Talks at 2F Auditorium Chair(s): Fuyuki Ishikawa National Institute of Informatics

09:00 70m Keynote		Towards Privacy-Preserving Verification Main Plenaries / Invited Talks Ruzica Piskac Yale University

10:40 - 12:20	Session 6: SMT, SAT & Constraint SolvingResearch Track at 2F Auditorium Chair(s): Loes Kruger Radboud University

10:40 25m Talk		Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness Research Track Áron Ricardo Perez-Lopez Stanford University, Po-Chun Chien LMU Munich, Florian Lonsing Unaffiliated, Samantha Archer Stanford University, Ahmed Irfan SRI International, Clark Barrett Stanford University DOI Media Attached
11:05 25m Talk		SAT-Based Syndrome Decoding and Low-Weight Codewords Research Track Carl Berton Laboratoire MIS UR 4290, Université de Picardie Jules Verne, Sami Cherif Laboratoire MIS UR 4290, Université de Picardie Jules Verne, Claire Delaplace Laboratoire MIS UR 4290, Université de Picardie Jules Verne
11:30 25m Talk		Certifying Constraints in Hardware Model Checking Research Track Nils Froleyks KU Leuven, Emily Yu Leiden University, Armin Biere University of Freiburg, Germany, Keijo Heljanko University of Helsinki
11:55 25m Talk		Highly Incremental: A Simple Programmatic Approach for Many Objectives Research Track Philipp Schröer RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University

13:50 - 15:30	Session 8: Model Checking & Program SynthesisResearch Track at 2F Auditorium Chair(s): Reiner Hähnle TU Darmstadt

13:50 25m Talk		Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking Research Track Radu-Florin Tulcan TU Wien, Rose Bohrer National Institute of Advanced Industrial Science and Technology (AIST), Japan, Yoàv Montacute National Institute of Informatics, Kevin Zhou National Institute of Informatics, Yusuke Kawamoto National Institute of Advanced Industrial Science and Technology (AIST), Japan, Ichiro Hasuo National Institute of Informatics, Japan
14:15 25m Talk		Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking Research Track Arnd Hartmanns University of Twente, Tim Quatmann RWTH Aachen University, Mark van Wijk University of Twente
14:40 25m Talk		Performance Heuristics for GR(1) Unrealizable Core Computation Research Track Shachaf Cohen Tel Aviv University, Shahar Maoz Tel Aviv University
15:05 25m Talk		Accelerating Kind Realizability: A Multi-Stage Incremental Realizability Checking Framework Research Track Sirui Liu College of Computer Science, National University of DefenseTechnology, Changsha, China, Wei Dong National University of Defense Technology

16:10 - 17:50	Session 10: Distributed Systems & Fault Tolerance Research Track at 2F Auditorium Chair(s): Matthias Volk Eindhoven University of Technology

16:10 25m Talk		A Formal Framework for Predicting Distributed System Performance under Faults Research Track Ziwei Zhou East China Normal University, Si Liu Texas A&M University, Zhou Zhou East China Normal University, Peixin Wang East China Normal University, Min Zhang East China Normal University
16:35 25m Talk		Fast SMT-Based Fault Tolerance Verification for Wide Area Networks Research Track Ning Kang Xi'an Jiaotong University, Peng Zhang Xi'an Jiaotong University, Hao Li Xi'an Jiaotong University, Jianyuan Zhang Xi'an Jiaotong University
17:00 25m Talk		A Refined Ordering Consistency Theory: Full Sequential Consistency and Generalized Preventive Reasoning Research Track Zhiheng Cai Tsinghua University, Zhihang Sun Tsinghua University, Fei He Tsinghua University
17:25 25m Talk		BDD-based Deadlock Prevention for Automated Guided Vehicles in Warehouse Logistics Research Track Benjamin von Berg Graz University of Technology, Bernhard Aichernig Johannes Kepler University, Linz, Fabian Wedenik KNAPP AG

17:55 - 18:10	FM 2026 Closing and FM 2027 AnnouncementMain Plenaries / Invited Talks at 2F Auditorium

17:55 7m Talk		FM 2026 Closing Main Plenaries / Invited Talks
18:02 7m Talk		FM 2027 Announcement Main Plenaries / Invited Talks

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


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30
2F Auditorium	Main Plenaries / Invited Talks FM Opening			Main Plenaries / Invited Talks FM/ABZ Keynote: Ichiro Hasuo														Main Plenaries / Invited Talks FME Lucas Award										Research Track Session 1: Information Flow Verification																															Main Plenaries / Invited Talks FM Industry Keynote: Daniel Kroening																				Journal First Journal-First																TAP Track TAP Session 1: Formal Languages, Reachability, and Program Verification

Thu 21 May
Displayed time zone: Osaka, Sapporo, Tokyo change


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30
2F Auditorium	Main Plenaries / Invited Talks FM/TAP Keynote: Cristian Cadar																				Research Track Session 2: Neural Networks Verification																																										Community Sessions FM4All & ACM Reference Curriculum																							Research Track Session 4: LLMs Formal Methods

Fri 22 May
Displayed time zone: Osaka, Sapporo, Tokyo change


Room	9:00						30						10:00						30						11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30
2F Auditorium	Main Plenaries / Invited Talks FM Keynote: Ruzica Piskac																				Research Track Session 6: SMT, SAT & Constraint Solving																																						Research Track Session 8: Model Checking & Program Synthesis																												Research Track Session 10: Distributed Systems & Fault Tolerance																					Main Plenaries / Invited Talks FM 2026 Closing and FM 2027 Announcement

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


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45			18:00			15			30			45
2F Auditorium	FM Main Plenaries / Invited Talks FM 2026 Opening 09:00 - 09:15			FM Main Plenaries / Invited Talks Cutting out FM Angles from the Jungle of Automated Driving 09:15 - 10:25																								FM Research Track Differential Verification of Information Flow in SEAndroid Policies 11:15 - 11:40					FM Research Track History-Constrained Systems 11:40 - 12:05					FM Research Track FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines 12:05 - 12:30																					FM Main Plenaries / Invited Talks The Industrial Perspective on GenAI for Formal Methods 13:50 - 15:00																				FM Journal First Journal-First Opening Talk 15:30 - 15:35	FM Journal First Modelling and Analysing Routing Protocols Diagrammatically with Bigraphs 15:35 - 16:00					FM Journal First Memory Consistency and Program Transformations 16:00 - 16:25										FM TAP Track Correct-by-Construction Dynamic Reachability: A Galois-Connected Approa ... 16:50 - 17:15					FM TAP Track EUF-based Solving Dyck-Reachability with Applications to Static Analysis 17:15 - 17:40					FM TAP Track Towards Formally Verified Smart Contracts Compilation 17:40 - 18:05

Thu 21 May
Displayed time zone: Osaka, Sapporo, Tokyo change


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45
2F Auditorium	FM Main Plenaries / Invited Talks Testing and Analysis in the AI Era 09:00 - 10:10																				FM Research Track Exact Verification of Graph Neural Networks with Incremental Constraint ... 10:40 - 11:05					FM Research Track Formal Reasoning About Confidence and Automated Verification of Neural ... 11:05 - 11:30					FM Research Track Mining Verdict Boundaries for Neural Network Verification 11:30 - 11:55					FM Research Track SAPSE-Synergy: Balancing Formal Soundness and Empirical Coverage in Neu ... 11:55 - 12:20																											FM Community Sessions FM4All - FME Guidelines for Teaching Formal Methods as a Knowledge Area ... 14:10 - 15:35																							FM Research Track Can LLM Aid in Solving Constraints with Inductive Definitions? 16:05 - 16:30					FM Research Track Towards Language Model Guided TLA+ Proof Automation 16:30 - 16:55					FM Research Track Validating Formal Specifications with LLM-generated Test Cases 16:55 - 17:20					FM Research Track ModelWisdom: An Integrated Toolkit for TLA+ Model Visualization, Digest ... 17:20 - 17:45

Fri 22 May
Displayed time zone: Osaka, Sapporo, Tokyo change


Room	9:00			15			30			45			10:00			15			30			45			11:00			15			30			45			12:00			15			30			45			13:00			15			30			45			14:00			15			30			45			15:00			15			30			45			16:00			15			30			45			17:00			15			30			45			18:00			15			30			45
2F Auditorium	FM Main Plenaries / Invited Talks Towards Privacy-Preserving Verification 09:00 - 10:10																				FM Research Track Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness 10:40 - 11:05					FM Research Track SAT-Based Syndrome Decoding and Low-Weight Codewords 11:05 - 11:30					FM Research Track Certifying Constraints in Hardware Model Checking 11:30 - 11:55					FM Research Track Highly Incremental: A Simple Programmatic Approach for Many Objectives 11:55 - 12:20																							FM Research Track Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and M ... 13:50 - 14:15					FM Research Track Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking 14:15 - 14:40					FM Research Track Performance Heuristics for GR(1) Unrealizable Core Computation 14:40 - 15:05					FM Research Track Accelerating Kind Realizability: A Multi-Stage Incremental Realizabilit ... 15:05 - 15:30													FM Research Track A Formal Framework for Predicting Distributed System Performance under ... 16:10 - 16:35					FM Research Track Fast SMT-Based Fault Tolerance Verification for Wide Area Networks 16:35 - 17:00					FM Research Track A Refined Ordering Consistency Theory: Full Sequential Consistency and ... 17:00 - 17:25					FM Research Track BDD-based Deadlock Prevention for Automated Guided Vehicles in Warehous ... 17:25 - 17:50						FM Main Plenaries / Invited Talks FM 2026 Closing 17:55 - 18:02	FM Main Plenaries / Invited Talks FM 2027 Announcement 18:02 - 18:10

Room information: 2F Auditorium

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

Thu 21 May
Displayed time zone: Osaka, Sapporo, Tokyo change

Fri 22 May
Displayed time zone: Osaka, Sapporo, Tokyo change

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

Main Plenaries / Invited Talks

Main Plenaries / Invited Talks

Main Plenaries / Invited Talks

Research Track

Main Plenaries / Invited Talks

Journal First

TAP Track

Thu 21 May
Displayed time zone: Osaka, Sapporo, Tokyo change

Main Plenaries / Invited Talks

Research Track

Community Sessions

Research Track

Fri 22 May
Displayed time zone: Osaka, Sapporo, Tokyo change

Main Plenaries / Invited Talks

Research Track

Research Track

Research Track

Main Plenaries / Invited Talks

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

Thu 21 May
Displayed time zone: Osaka, Sapporo, Tokyo change

Fri 22 May
Displayed time zone: Osaka, Sapporo, Tokyo change

Tracks

Room information: 2F Auditorium

Program Display Configuration

Wed 20 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

Thu 21 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

Fri 22 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

Wed 20 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

Main Plenaries / Invited Talks

Main Plenaries / Invited Talks

Main Plenaries / Invited Talks

Research Track

Main Plenaries / Invited Talks

Journal First

TAP Track

Thu 21 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

Main Plenaries / Invited Talks

Research Track

Community Sessions

Research Track

Fri 22 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

Main Plenaries / Invited Talks

Research Track

Research Track

Research Track

Main Plenaries / Invited Talks

Wed 20 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

Thu 21 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

Fri 22 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

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

Thu 21 May
Displayed time zone: Osaka, Sapporo, Tokyo change

Fri 22 May
Displayed time zone: Osaka, Sapporo, Tokyo change

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

Thu 21 May
Displayed time zone: Osaka, Sapporo, Tokyo change

Fri 22 May
Displayed time zone: Osaka, Sapporo, Tokyo change

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

Thu 21 May
Displayed time zone: Osaka, Sapporo, Tokyo change

Fri 22 May
Displayed time zone: Osaka, Sapporo, Tokyo change