Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Mon 18 MayDisplayed time zone: Osaka, Sapporo, Tokyo change
Mon 18 May
Displayed time zone: Osaka, Sapporo, Tokyo change
08:45 - 09:15 | |||
08:45 30mRegistration | Registration Services | ||
09:15 - 10:45 | |||
09:15 90mTalk | AIPV session 1 talks Workshop: AIPV | ||
09:15 - 10:45 | Tutorial 2: The SLEEC Framework for Normative Requirements Engineering (Part 1)Tutorials at 2F Conf Room 3 | ||
09:15 90mTutorial | The SLEEC Framework for Normative Requirements Engineering Tutorials Pedro Ribeiro University of York, UK, Radu Calinescu University of York, UK, Ana Cavalcanti University of York, Marsha Chechik University of Toronto, Sinem Getir Yaman University of York, UK, Lina Marsso Polytechnique Montreal, Isobel Standen University of York, Beverley Townsend University of York | ||
09:15 - 10:45 | Tutorial 1: Distributed Runtime Verification in Proximity-based Networks: A Tutorial on the Aggregate Programming Approach (Part 1)Tutorials at 2F Conf Room 4 | ||
09:15 90mTutorial | Distributed Runtime Verification in Proximity-based Networks: A Tutorial on the Aggregate Programming Approach Tutorials Giorgio Audrito Università di Torino, Ferruccio Damiani University of Turin, Giordano Scarso University of Turin, Volker Stolz Høgskulen på Vestlandet, Gianluca Torta DOI Pre-print | ||
10:45 - 11:10 | |||
10:45 25mCoffee break | Break Services | ||
11:10 - 12:40 | Tutorial 2: The SLEEC Framework for Normative Requirements Engineering (Part 2)Tutorials at 2F Conf Room 3 | ||
11:10 90mTutorial | The SLEEC Framework for Normative Requirements Engineering Tutorials Pedro Ribeiro University of York, UK, Radu Calinescu University of York, UK, Ana Cavalcanti University of York, Marsha Chechik University of Toronto, Sinem Getir Yaman University of York, UK, Lina Marsso Polytechnique Montreal, Isobel Standen University of York, Beverley Townsend University of York | ||
11:10 - 12:40 | Tutorial 1: Distributed Runtime Verification in Proximity-based Networks: A Tutorial on the Aggregate Programming Approach (Part 2)Tutorials at 2F Conf Room 4 | ||
11:10 90mTutorial | Distributed Runtime Verification in Proximity-based Networks: A Tutorial on the Aggregate Programming Approach Tutorials Giorgio Audrito Università di Torino, Ferruccio Damiani University of Turin, Giordano Scarso University of Turin, Volker Stolz Høgskulen på Vestlandet, Gianluca Torta DOI Pre-print | ||
11:15 - 12:45 | |||
11:15 90mTalk | AIPV session 2 talks Workshop: AIPV | ||
12:40 - 14:00 | |||
12:40 80mLunch | Lunch Services | ||
14:00 - 15:30 | |||
14:00 90mTalk | AIPV session 3 talks Workshop: AIPV | ||
14:00 - 14:30 | |||
14:00 30mKeynote | Overture Keynote Talk Workshop: Overture Keijiro Araki Kyushu Institute of Technology, Japan | ||
14:00 - 16:05 | |||
14:00 25mTalk | chronoEvent-B: A Rodin Plugin for Timed Constraints in Event-B Workshop: Rodin | ||
14:25 25mTalk | Rust Toolchain for Event-B with Language Server Support Workshop: Rodin | ||
14:50 25mTalk | A theory for defining and handling matrices in Event-B Workshop: Rodin | ||
15:15 25mTalk | Enhancing EB4EB Framework by Introducing Lexicographic Variants Workshop: Rodin | ||
15:40 25mTalk | Automated transformation of Event-B machines into EB4EB deep instances Workshop: Rodin | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Probabilistic Model Checking Taken by Storm Tutorials Matthias Volk Eindhoven University of Technology, Linus Heck Radboud University, Sebastian Junges Radboud University, Joost-Pieter Katoen RWTH Aachen University, Tim Quatmann RWTH Aachen University Pre-print | ||
14:00 - 15:30 | Tutorial 3: Reasoning over Relaxed Shared Memory Models: A Tutorial (Part 1)Tutorials at 2F Conf Room 4 | ||
14:00 90mTutorial | Reasoning over Relaxed Shared Memory Models: A Tutorial Tutorials Brijesh Dongol University of Surrey Pre-print | ||
15:00 - 15:40 | |||
15:00 20mTalk | Overture Tool Overview Workshop: Overture Peter Gorm Larsen Aarhus University | ||
15:20 20mTalk | ViennaTalk Overview Workshop: Overture Tomohiro Oda Software Research Associates, Inc. | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Services | ||
16:00 - 17:50 | |||
16:00 1h50mTalk | AIPV session 4 talks Workshop: AIPV | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Probabilistic Model Checking Taken by Storm Tutorials Matthias Volk Eindhoven University of Technology, Linus Heck Radboud University, Sebastian Junges Radboud University, Joost-Pieter Katoen RWTH Aachen University, Tim Quatmann RWTH Aachen University Pre-print | ||
16:00 - 17:30 | Tutorial 3: Reasoning over Relaxed Shared Memory Models: A Tutorial (Part 2)Tutorials at 2F Conf Room 4 | ||
16:00 90mTutorial | Reasoning over Relaxed Shared Memory Models: A Tutorial Tutorials Brijesh Dongol University of Surrey Pre-print | ||
16:20 - 18:00 | |||
16:20 25mTalk | Inductive Set Construction using instantiation and Rodin Workshop: Rodin | ||
16:45 25mTalk | An Event-B Sequent Prover in Prolog and ProB Workshop: Rodin | ||
17:10 25mTalk | Updates in the Rodin plug-in ecosystem Workshop: Rodin | ||
17:35 25mTalk | Modeling and Proving the Parallel Climbers Puzzle in Event-B Workshop: Rodin | ||
16:40 - 17:40 | |||
16:40 30mTalk | Trace-Based Execution-Level Observability of VDM-SL Specifications Workshop: Overture | ||
17:10 30mTalk | Executing Kapture's Templates in VDM Workshop: Overture Leo Freitas Newcastle University, Joe Hare Newcastle University, Ken Pierce The University of Newcastle | ||
18:00 - 19:00 | |||
18:00 30mTalk | Further Progress Towards Operation Proof Obligation Generation for VDM Workshop: Overture | ||
18:30 30mTalk | A System-of-Systems Case Study for the Verification of Composed Digital Twins Workshop: Overture Mennatullah Khedr Newcastle University, Mengwei Xu University of Newcastle, John Fitzgerald Newcastle University, Peter Gorm Larsen Aarhus University | ||
18:00 - 20:00 | |||
18:00 2hTalk | AIPV Reception Workshop: AIPV | ||
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 60mTalk | Gedenkschrift for Jean-Raymond AbrialABZ ABZ | ||
Tue 19 MayDisplayed time zone: Osaka, Sapporo, Tokyo change
Tue 19 May
Displayed time zone: Osaka, Sapporo, Tokyo change
08:30 - 09:00 | |||
08:30 30mRegistration | Registration Services | ||
08:50 - 09:00 | |||
08:50 10mTalk | Doctoral Symposium Opening Doctoral Symposium | ||
09:00 - 10:30 | |||
09:00 90mTalk | AIPV session 5 talks Workshop: AIPV | ||
09:00 - 10:30 | DS Session 1: System-Level Verification and Security ApplicationsDoctoral Symposium at 2F Conf Room 1 | ||
09:00 30mTalk | Revealing Intent–Implementation Gaps in Schedulers via Learning-Based Fuzzing Doctoral Symposium Akira Hasegawa Japan Advanced Institute of Science and Technology | ||
09:30 30mTalk | Static Analysis and Synthesis of Layered Attestation Protocols Doctoral Symposium Will Thomas University of Kansas | ||
10:00 30mTalk | Towards a Bigraph-Based Digital Twin Framework for Multi-UAV Coordination in AAM Doctoral Symposium Tianxiong Zhang Chair of Software Technology, Technische Universität Dresden | ||
09:00 - 10:30 | Tutorial 6: Mixed Flow-Sensitive Static Analysis: Engineering Modularity (Part 1)Tutorials at 2F Conf Room 2 | ||
09:00 90mTutorial | Mixed Flow-Sensitive Static Analysis: Engineering Modularity Tutorials Helmut Seidl TU Munich, Vesal Vojdani University of Tartu, Julian Erhard TU Munich; LMU Munich, Michael Schwarz National University of Singapore | ||
09:00 - 10:30 | |||
09:00 90mTutorial | Formally Explaining Neural Network Classification Tutorials Tomáš Kolárik University of Lugano, Natasha Sharygina USI Lugano, Switzerland, Faezeh Labbaf University of Lugano, Fabrizio Leopardi University of Lugano, Grigory Fedyukovich Florida State University, Michael Wand Dalle Molle Institute for Artificial Intelligence USI-SUPSI | ||
09:00 - 09:10 | |||
09:00 10mTalk | ABZ Opening ABZ | ||
09:00 - 09:10 | |||
09:10 - 10:10 | |||
09:10 60mKeynote | Practical Applications of Formal Methods to Automotive Systems: From In-Vehicle Systems to Autonomous Driving ABZ Toshiaki Aoki JAIST | ||
09:10 - 10:30 | |||
09:10 25mTalk | Autograding Weakest Precondition Proofs and Dafny Specifications Workshop: FMTea | ||
09:35 25mTalk | Automatic Assessment and Feedback on Undergraduates’ Structural Induction Proofs Workshop: FMTea Edward Sabinus Martin-Luther-University Halle-Wittenberg, Thomas Kühn Martin-Luther-University Halle-Wittenberg, Wolf Zimmermann Martin-Luther-University Halle-Wittenberg | ||
10:00 25mTalk | Seven-Year Activity to Introduce B-Method to Japanese Technical College Students Workshop: FMTea Takaomi Ohnishi National Institute of Technology, Tomakomai College, Japan, Yoshihiko Nakamura National Institute of Technology, Tomakomai College, Ryota Yamamoto National Institute of Technology, Tomakomai College | ||
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 25mTalk | A Method for Testing Partial-Order Reduction Theories in Alloy ABZ | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break Services | ||
11:00 - 12:30 | |||
11:00 90mTalk | AIPV session 6 talks Workshop: AIPV | ||
11:00 - 12:30 | |||
11:00 30mTalk | Towards verified memory allocator for Rust Doctoral Symposium Sinai Kakishita Japan Advanced Institute of Science and Technology | ||
11:30 30mTalk | Unifying Non-Atomicity for Weak Memory Models Doctoral Symposium Stepan Kuznetsov TU Braunschweig & Huawei Hilbert Research Center | ||
12:00 30mTalk | Formal Verification of Soundness and Completeness for Polygon zkEVM Doctoral Symposium | ||
11:00 - 12:30 | Tutorial 6: Mixed Flow-Sensitive Static Analysis: Engineering Modularity (Part 2)Tutorials at 2F Conf Room 2 | ||
11:00 90mTutorial | Mixed Flow-Sensitive Static Analysis: Engineering Modularity Tutorials Helmut Seidl TU Munich, Vesal Vojdani University of Tartu, Julian Erhard TU Munich; LMU Munich, Michael Schwarz National University of Singapore | ||
11:00 - 12:30 | |||
11:00 90mTutorial | Formally Explaining Neural Network Classification Tutorials Tomáš Kolárik University of Lugano, Natasha Sharygina USI Lugano, Switzerland, Faezeh Labbaf University of Lugano, Fabrizio Leopardi University of Lugano, Grigory Fedyukovich Florida State University, Michael Wand Dalle Molle Institute for Artificial Intelligence USI-SUPSI | ||
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 25mTalk | Identifying Design Flaws in a Lock-Free Task Pool with TLA+ ABZ | ||
11:25 25mTalk | Formal Modelling and Analysis of the ORAN O2 Interface in Alloy: Implications for NTN Deployment ABZ 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 25mTalk | Formal Verification of Healthcare Computer Network Architectures using Alloy and TLA+ ABZ Daniel Daukševič Institute of Computer Science, Vilnius University, Vilnius,Lithuania, Linas Laibinis Institute of Computer Science, Vilnius University, Vilnius,Lithuania | ||
12:15 15mTalk | Formal Verification of Decentralized Autonomous Organizations ABZ Simone Valentini University of Milan, Sowelu Avanzo University of Turin, Elvinia Riccobene Computer Science Dept., University of Milan | ||
11:00 - 12:00 | |||
11:00 60mKeynote | Teaching Logic with Specification Challenges Workshop: FMTea Alcino Cunha University of Minho; INESC TEC | ||
12:00 - 12:30 | |||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Services | ||
13:45 - 14:45 | |||
13:45 60mKeynote | Reasoning Beyond LLM: Formal Methods Agents ABZ Jin Song Dong National University of Singapore | ||
14:00 - 15:30 | |||
14:00 90mTalk | AIPV session 7 talks Workshop: AIPV | ||
14:00 - 15:30 | |||
14:00 90mTutorial | Digital Twins: a Briefing for Formalists Tutorials John Fitzgerald Newcastle University, Claudio Gomes Aarhus University, Denmark, Peter Gorm Larsen Aarhus University, Mikkel Schmidt Andersen Aarhus University, Santiago Gil Aarhus University, Morten Haahr Kristensen Aarhus University | ||
14:00 - 15:30 | Tutorial 7: Requirements Elicitation, Formalization, and Analysis with FRET: A Tutorial (Part 1)Tutorials at 2F Conf Room 3 | ||
14:00 90mTutorial | Requirements Elicitation, Formalization, and Analysis with FRET: A Tutorial Tutorials Anastasia Mavridou KBR / NASA Ames Research Center, Andreas Katis KBR / NASA Ames Research Center, Mari Aoki NASA, Marie Farrell The University of Manchester | ||
14:00 - 15:00 | |||
14:00 60mKeynote | Teaching Unifying Theories of Programming Workshop: FMTea Jim Woodcock University of York | ||
14:15 - 15:15 | |||
14:15 60mKeynote | Engineering Resilient Autonomous Systems with Formal Methods Doctoral Symposium | ||
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 25mTalk | Relational Verification of Identity Disclosure Using Alloy ABZ 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 25mTalk | Security-Minded Modelling and Verification of Autonomous Satellite Docking ABZ Juel Hussain University of Manchester, Marie Farrell The University of Manchester, Louise Dennis University of Manchester, Clare Dixon University of Manchester | ||
15:35 15mTalk | SHARCS: Refinement-Centric Hazard Analysis of Requirements for Critical Systems ABZ Asieh Salehi Fathabadi University of Southampton, Thai Son Hoang University of Southampton, Michael Butler University of Southampton | ||
15:00 - 15:30 | |||
15:15 - 15:45 | |||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break Services | ||
15:45 - 17:15 | |||
15:45 30mTalk | Cybersecurity Requirements Assurance in Critical Infrastructure Systems through the Application of Formal Verification and Artificial Intelligence-Based Methods Doctoral Symposium Daniel Daukševič Institute of Computer Science, Vilnius University, Vilnius,Lithuania | ||
16:15 30mTalk | Visualizing Neural Network Behaviors for Verification Doctoral Symposium Xiaolin Liu KTH Royal Institute of Technology | ||
16:45 30mTalk | Towards Characterizing Commit Patterns in Formally Verified Open-Source Projects Using LLM-based Classification Doctoral Symposium Soshi Inoue Kyoto Institute of Technology | ||
16:00 - 17:50 | |||
16:00 1h50mTalk | AIPV session 8 talks Workshop: AIPV | ||
16:00 - 17:30 | |||
16:00 90mTutorial | Digital Twins: a Briefing for Formalists Tutorials John Fitzgerald Newcastle University, Claudio Gomes Aarhus University, Denmark, Peter Gorm Larsen Aarhus University, Mikkel Schmidt Andersen Aarhus University, Santiago Gil Aarhus University, Morten Haahr Kristensen Aarhus University | ||
16:00 - 17:30 | Tutorial 7: Requirements Elicitation, Formalization, and Analysis with FRET: A Tutorial (Part 2)Tutorials at 2F Conf Room 3 | ||
16:00 90mTutorial | Requirements Elicitation, Formalization, and Analysis with FRET: A Tutorial Tutorials Anastasia Mavridou KBR / NASA Ames Research Center, Andreas Katis KBR / NASA Ames Research Center, Mari Aoki NASA, Marie Farrell The University of Manchester | ||
16:00 - 17:20 | |||
16:00 25mTalk | Learning Formal Methods through Project-Based Modeling of Concurrent Systems with Anemone Workshop: FMTea | ||
16:25 25mTalk | Teaching Frama-C for Cybersecurity Workshop: FMTea Julien Signoles Université Paris-Saclay, CEA, List | ||
16:50 25mTalk | VeHa: A Hybrid National Verification Hackathon for Better Formal Methods Education Workshop: FMTea Sergey Staroletov Polzunov Altai State Technical University, Dmitry Kondratyev A.P. Ershov Institute of Informatics Systems SB RAS, Vladimir Shelekhov A.P. Ershov Institute of Informatics Systems SB RAS, Alexander Kogtenkov Kaspersky Lab, Nikolay Shilov Innopolis University, Natalia Garanina Ivannikov Institute for System Programming of the RAS, Irina Shoshmina Peter the Great St. Petersburg Polytechnic University, Timofey Cherganov RusBITech-Astra LLC, Vasil Dyadov Kaspersky Lab | ||
16:15 - 17:20 | |||
16:15 25mTalk | Slicing Models for Equiconsistency with Alloy ABZ 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 25mTalk | Verifying Properties of State-Based Models using Constraint Programming ABZ 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 15mTalk | Why does it fail? Explanation of verification failures ABZ Lars-Henrik Eriksson Uppsala University | ||
17:15 - 17:25 | |||
17:20 - 17:30 | |||
17:25 - 17:30 | |||
17:25 5mTalk | Doctoral Symposium Closing Doctoral Symposium | ||
17:35 - 18:40 | |||
17:35 25mTalk | Encoding BDI Syntax with Theories in Event-B ABZ 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 25mTalk | Fuzzing executable ASMETA models ABZ | ||
18:25 15mTalk | Human-Centred Formal Verification: A Vision for Bridging Technical Rigour with Stakeholder Needs in Autonomous Systems ABZ | ||
18:45 - 20:15 | |||
18:45 90mDinner | ABZ Welcome Reception ABZ | ||
Wed 20 MayDisplayed time zone: Osaka, Sapporo, Tokyo change
Wed 20 May
Displayed time zone: Osaka, Sapporo, Tokyo change
08:30 - 09:00 | |||
08:30 30mRegistration | Registration Services | ||
09:00 - 09:15 | |||
09:00 15mTalk | FM 2026 Opening Main Plenaries / Invited Talks | ||
09:15 - 10:25 | |||
09:15 70mKeynote | 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 | |||
10:45 - 11:15 | |||
10:45 30mCoffee break | Break Services | ||
11:15 - 12:15 | |||
11:15 60mKeynote | Systematic Development of Distributed Algorithms using Event-B - Experiences, reviews and prospects - ABZ Dominique Mery Université de Lorraine, CNRS, INRIA / LORIA & Telecom Nancy, France | ||
11:15 - 12:30 | Session 1: Information Flow VerificationResearch Track at 2F Auditorium Chair(s): Graeme Smith The University of Queensland | ||
11:15 25mTalk | 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 25mTalk | 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 25mTalk | FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines Research Track Xindi Zhang , Furong Ye LIACS, Leiden University, Zhihan Chen Institute of Software, Chinese Academy of Sciences, Shaowei Cai Institute of Software at Chinese Academy of Sciences | ||
11:15 - 11:30 | |||
11:30 - 12:30 | Industry Session 1: Automated Synthesis, Optimization, and CertificationIndustry Day at 2F Conference Room Chair(s): Naoto Sato Hitachi, Ltd. | ||
11:30 20mIndustry talk | Efficient Multi-Level Mine Dewatering Using UPPAAL Stratego Industry Day Muhammad Naeem Mälardalen University, Västerås, Sweden, Cristina Seceleanu Mälardalen University, Alf Isaksson ABB AB, Tiberiu Seceleanu Mälardalen University | ||
11:50 20mIndustry talk | (Extended Abstract) Verifiably UX Compliant and User-Intent Layout Generation Industry Day | ||
12:10 20mIndustry talk | Formal Verification for Security Certification: From a First Success to Sustainable Industrial Usage Industry Day Adel Djoudi Thales Cybersecurity and Digital Identity, Nikolai Kosmatov Thales Research & Technology | ||
12:15 - 12:30 | |||
12:15 15mTalk | Overview of Gedenkschrift for Jean-Raymond Abrial ABZ | ||
12:30 - 13:50 | |||
12:30 80mLunch | Lunch Services | ||
13:50 - 15:00 | |||
13:50 70mKeynote | The Industrial Perspective on GenAI for Formal Methods Main Plenaries / Invited Talks Daniel Kroening Amazon | ||
15:00 - 15:30 | |||
15:00 30mCoffee break | Break Services | ||
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 25mTalk | Counterexample-Guided Interval Weakening ABZ 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 25mTalk | Specification and Analysis of Ethical Requirements in Autonomous Systems using Abstract State Machines ABZ 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 15mTalk | Evaluating the Practical Impact of Parallelism in Asmeta ABZ 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 | ||
15:30 - 16:25 | |||
15:30 5mTalk | Journal-First Opening Talk Journal First | ||
15:35 25mTalk | Modelling and Analysing Routing Protocols Diagrammatically with Bigraphs Journal First Michele Sevegnani University of Glasgow Link to publication | ||
16:00 25mTalk | Memory Consistency and Program Transformations Journal First Akshay Gopalakrishnan McGill University Link to publication | ||
15:30 - 16:35 | Industry Session 2: Code-Level Verification, Repair, and TestingIndustry Day at 2F Conference Room Chair(s): Cristina Seceleanu Mälardalen University | ||
15:30 20mIndustry talk | Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel Industry Day Tianqi Zhao Zhongguancun Laboratory, Qinxiang Cao Shanghai Jiao Tong University, Shenghua Feng Zhongguancun Laboratory, Minghui Zhou Peking University, Naijun Zhan Peking University; Zhongguancun Laboratory, Yongzhi Cao Peking University, Junfeng Zhao Inner Mongolia University, Haiyan Zhao Peking University, Hao Wang Shenzhen Kaihong Digital Industry Development Co., Ltd., Zhenjiang Hu Peking University | ||
15:50 20mIndustry talk | Robustness Semantics based Configuration Bug Fixing for Automated Driving Systems Industry Day Xiaodong Zhang University of Chinese Academy of Science, Songyang Yan Xi'an Jiaotong University and The University of Tokyo, Zijiang Yang University of Science and Technology of China and Synkrotron, Inc. | ||
16:10 20mIndustry talk | SeaCoral: A Collaborative Test Generation Toolset for Industrial Orchestration of Testing Tools Industry Day Nicolas Berthier OCamlPro, Steven de Oliveira OCamlPro, Nikolai Kosmatov Thales Research & Technology, Delphine Longuet Thales Research & Technology | ||
15:30 - 16:30 | |||
15:30 60mMeeting | FAC Editorial Board Meeting (Member Only) Community Sessions | ||
16:35 - 16:50 | |||
16:35 15mCoffee break | Break Services | ||
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 25mTalk | Formal Modeling and Analysis of a Planetary Rover under Abnormal Scenarios with Quint ABZ 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 25mTalk | Can Large Language Models Support Modeling Systems with ASMETA? A Case Study with a Planetary Rover ABZ Andrea Bombarda University of Bergamo, Silvia Bonfanti University of Bergamo, Angelo Gargantini University of Bergamo, Nico Pellegrinelli University of Bergamo | ||
17:35 25mTalk | A Spectabular Model of an Automotive Adaptive Exterior Light System ABZ Emil Sekerinski McMaster University, Canada | ||
16:50 - 18:05 | |||
16:50 25mTalk | 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 25mTalk | 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 25mTalk | Towards Formally Verified Smart Contracts Compilation TAP Track Elvira Albert , Samir Genaim Universidad Complutense de Madrid, Enrique Martin-Martin Universidad Complutense de Madrid | ||
16:50 - 17:50 | Industry Session 3: AI-Assisted Requirements Engineering and Early-Stage AnalysisIndustry Day at 2F Conference Room Chair(s): Jeroen Keiren Eindhoven University of Technology, The Netherlands | ||
16:50 20mIndustry talk | Automated ITL Specification Generation from Industrial Aerospace Requirements Industry Day Zhi Ma Xidian University, Xiao Liang Xidian University, Cheng Wen Xidian University, Rui Chen Beijing Institute of Control Engineering; Beijing Sunwise Information Technology, Bin Gu Beijing Institute of Control Engineering, Shengchao Qin Xidian University, Cong Tian Xidian University, Mengfei Yang China Academy of Space Technology | ||
17:10 20mIndustry talk | Shift-Left Requirements Verification: Integrating LLMs and Formal Methods for Automotive Systems Industry Day Zi Pong Lim Nanyang Technological University, bozhi wu Singapore Management University, Yon Shin Teo Aumovio SE, Shang-Wei LIN Singapore Institute of Technology, Yi Li Nanyang Technological University | ||
17:30 20mIndustry talk | Pragmatic Uses of AI in Formal Methods–Based Railway Projects: Early Lessons and Perspectives Industry Day | ||
17:50 - 18:05 | Industry Day ClosingIndustry Day at 2F Conference Room Chair(s): Jeroen Keiren Eindhoven University of Technology, The Netherlands | ||
18:00 - 18:10 | |||
18:00 10mTalk | ABZ Award and Closing ABZ | ||
18:10 - 18:30 | Walk to Reception at TKPMain Plenaries / Invited Talks at Reception Venue: TKP Garden City PREMIUM Jinbocho | ||
18:10 20mDinner | Move to Reception Main Plenaries / Invited Talks | ||
18:30 - 20:30 | |||
18:30 2hDinner | Reception Main Plenaries / Invited Talks | ||
Thu 21 MayDisplayed time zone: Osaka, Sapporo, Tokyo change
Thu 21 May
Displayed time zone: Osaka, Sapporo, Tokyo change
08:30 - 09:00 | |||
08:30 30mRegistration | Registration Services | ||
09:00 - 10:10 | |||
09:00 70mKeynote | Testing and Analysis in the AI Era Main Plenaries / Invited Talks Cristian Cadar Imperial College London | ||
10:10 - 10:40 | |||
10:10 30mCoffee break | Break Services | ||
10:40 - 12:30 | |||
10:40 25mTalk | 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 25mTalk | 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 25mTalk | 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 25mTalk | 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 | ||
10:40 - 12:30 | Session 3: Concurrency & Memory ModelsResearch Track at 2F Conference Room Chair(s): Brijesh Dongol University of Surrey | ||
10:40 25mTalk | Automatic Memory Management for Dataflows Research Track | ||
11:05 25mTalk | Complexity of Consistency Testing for the Release-Acquire Semantics Research Track R Govind The Institute of Mathematical Sciences, Shankaranarayanan Krishna IIT Bombay, Sanchari Sil Chennai Mathematical Institute, B Srivathsan Chennai Mathematical Institute | ||
11:30 25mTalk | Towards Proving Liveness on Weak Memory Research Track Lara Bargmann University of Oldenburg, Heike Wehrheim Carl von Ossietzky Universität Oldenburg / University of Oldenburg | ||
11:55 25mTalk | Generating Rely-Guarantee Conditions with the Conditional-Writes Domain Research Track | ||
12:30 - 14:10 | |||
12:30 1h40mLunch | Lunch Services | ||
12:30 - 14:10 | |||
12:30 1h40mLunch | FME Business Meeting Community Sessions | ||
14:10 - 15:35 | |||
14:10 85mTalk | FM4All - FME Guidelines for Teaching Formal Methods as a Knowledge Area in the ACM Curriculum Community Sessions Luigia Petre Åbo Akademi University | ||
14:10 - 15:35 | |||
14:10 25mTalk | Selective Concolic Testing TAP Track Guofeng Zhang College of Computer, National University of Defense Technology, Zhenbang Chen College of Computer, National University of Defense Technology, Ziqi Shuai School of Computer, National University of Defense Technology, China, Jun Sun Singapore Management University, Weijiang Hong National University of Defense Technology, Changsha, China, Yufeng Zhang Hunan University, Ji Wang National University of Defense Technology, Yang Liu | ||
14:35 25mTalk | From Execution to Necessity: Proof-Based Metrics for Code Coverage TAP Track | ||
15:00 25mTalk | Active Automata Learning with Noisy Data: From Big to Small Data TAP Track Felix Wallner Johannes Kepler University Linz, Bernhard Aichernig Johannes Kepler University, Linz, Benjamin von Berg Graz University of Technology, Maximilian Rindler Graz University of Technology | ||
15:35 - 16:05 | |||
15:35 30mCoffee break | Break Services | ||
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 25mTalk | 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 25mTalk | Towards Language Model Guided TLA+ Proof Automation Research Track | ||
16:55 25mResearch paper | Validating Formal Specifications with LLM-generated Test Cases Research Track Pre-print | ||
17:20 25mTalk | 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 | ||
16:05 - 17:55 | Session 5: Logic and SemanticsResearch Track at 2F Conference Room Chair(s): Zhenya Zhang Kyushu University | ||
16:05 25mTalk | A General Framework for Robust Quantitative Semantics of Signal Temporal Logic Research Track Jiawei Chen University of Michigan at Ann Arbor, José Luiz Vargas de Mendonça University of Michigan at Ann Arbor, Konstantinos Mamouras Rice University, Jean-Baptiste Jeannin University of Michigan at Ann Arbor | ||
16:30 25mTalk | Quantitative Monitoring of Signal First-Order Logic Research Track Marek Chalupa Institute of Science and Technology Austria, Thomas A. Henzinger Institute of Science and Technology Austria (ISTA), N. Ege Saraç CISPA Helmholtz Center for Information Security, Emily Yu Leiden University | ||
16:55 25mTalk | Reachability-guided Abstraction Refinement Research Track Pierre Ganty IMDEA Software Institute, Spain, Nicolas Manini IMDEA Software Institute, Francesco Ranzato University of Padova | ||
17:20 25mTalk | Maximum Realizability for LTL Modulo Theories Research Track | ||
17:55 - 18:15 | Bus to the Banquet at ChinzansoMain Plenaries / Invited Talks at Outside: Bus in Front of the Venue Building | ||
17:55 20mDinner | Move to Banquet Main Plenaries / Invited Talks | ||
19:00 - 21:00 | |||
19:00 2hDinner | Banquet Main Plenaries / Invited Talks | ||
Fri 22 MayDisplayed time zone: Osaka, Sapporo, Tokyo change
Fri 22 May
Displayed time zone: Osaka, Sapporo, Tokyo change
08:30 - 09:00 | |||
08:30 30mRegistration | Registration Services | ||
09:00 - 10:10 | |||
09:00 70mKeynote | Towards Privacy-Preserving Verification Main Plenaries / Invited Talks Ruzica Piskac Yale University | ||
10:10 - 10:40 | |||
10:10 30mCoffee break | Break Services | ||
10:40 - 12:20 | |||
10:40 25mTalk | 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 | ||
11:05 25mTalk | 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 25mTalk | 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 25mTalk | Highly Incremental: A Simple Programmatic Approach for Many Objectives Research Track | ||
10:40 - 12:20 | Session 7: Programming Languages & Program LogicResearch Track at 2F Conference Room Chair(s): Masaki Waga Kyoto University | ||
10:40 25mTalk | RustyDL: A Program Logic for Rust Research Track | ||
11:05 25mTalk | Array-Carrying Symbolic Execution for Function Contract Generation Research Track Weijie Lu Shanghai Jiao Tong University, Jingyu Ke , Hongfei Fu Shanghai Jiao Tong University, Zhouyue Sun Shanghai Jiao Tong University, Yi Zhou Shanghai Jiao Tong University, Guoqiang Li Shanghai Jiao Tong University, Haokun Li Peking University | ||
11:30 25mTalk | A Framework for the Interoperable Specification and Verification of Encapsulated Data Structures Research Track Wolfram Pfeifer Karlsruhe Institute of Technology (KIT), Werner Dietl University of Waterloo, Mattias Ulbrich KIT | ||
11:55 25mTalk | Verifying Sampling Algorithms via Distributional Invariants Research Track Kevin Batz Cornell University, Joost-Pieter Katoen RWTH Aachen University, Tobias Winkler RWTH Aachen University, Daniel Zilken RWTH Aachen University | ||
12:30 - 13:50 | |||
12:30 80mLunch | Lunch Services | ||
13:50 - 15:30 | Session 8: Model Checking & Program SynthesisResearch Track at 2F Auditorium Chair(s): Reiner Hähnle TU Darmstadt | ||
13:50 25mTalk | 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 25mTalk | 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 25mTalk | Performance Heuristics for GR(1) Unrealizable Core Computation Research Track | ||
15:05 25mTalk | Accelerating Kind Realizability: A Multi-Stage Incremental Realizability Checking Framework Research Track | ||
13:50 - 15:30 | Session 9: Automata & Reactive ModelsResearch Track at 2F Conference Room Chair(s): Nikolai Kosmatov Thales Research & Technology | ||
13:50 25mTalk | Asynchronous Team Automata Research Track Davide Basile CNR-ISTI, Maurice ter Beek CNR-ISTI Pisa, Italy, José Proença CISTER & Faculty of Sciences, University of Porto | ||
14:15 25mTalk | Error-awareness Accelerates Active Automata Learning Research Track Loes Kruger Radboud University, Sebastian Junges Radboud University, Jurriaan Rot Radboud University Nijmegen | ||
14:40 25mTalk | Pacing Types for Asynchronous Stream Equations Research Track Arthur Correnson CISPA Helmholtz Center for Information Security, Florian Kohn CISPA, Jan Baumeister CISPA Helmholtz Center for Information Security, Bernd Finkbeiner CISPA Helmholtz Center for Information Security | ||
15:05 25mTalk | Specializing anti-unification for interaction models composition via gate connections Research Track | ||
15:40 - 16:10 | |||
15:40 30mCoffee break | Break Services | ||
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 25mTalk | 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 25mTalk | 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 25mTalk | A Refined Ordering Consistency Theory: Full Sequential Consistency and Generalized Preventive Reasoning Research Track | ||
17:25 25mTalk | 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 | ||
16:10 - 17:50 | Session 11: Cyber-Physical & Robotics SystemsResearch Track at 2F Conference Room Chair(s): Maurice ter Beek CNR-ISTI Pisa, Italy | ||
16:10 25mTalk | Incremental Synthesis of Safe Controller Guided by Learning-Enabled Barrier Certificates with Efficient LP Verification Research Track Niuniu Qi East China Normal University, Hanrui Zhao National University of Defense Technology, Zhengfeng Yang East China Normal University, Xia Zeng Southwest University, Mengxin Ren East China Normal University, Chao Peng East China Normal University, Zhiming Liu Southwest University | ||
16:35 25mTalk | Test Coverage of Automated Robotic Systems in Open World Environments Research Track Lukas Westhofen DLR e.V. Institute of Systems Engineering for Future Mobility, Till Schallau TU Dortmund University, Dominik Schmid TU Dortmund University, Stefan Naujokat TU Dortmund University, Falk Howar TU Dortmund University, Danel Neider TU Dortmund University | ||
17:00 25mTalk | Exact Moment Estimation of Stochastic Differential Dynamics Research Track Shenghua Feng Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Jie An Institute of Software Chinese Academy of Sciences, Naijun Zhan Peking University; Zhongguancun Laboratory, Fanjiang Xu Institute of Software at Chinese Academy of Sciences | ||
17:25 25mTalk | QSeqSim: A Symbolic Simulator for Qiskit While Loops using Sequential Quantum Circuits Research Track Zihao Li University of Chinese Academy of Sciences, Ji Guan Institute of Software, Chinese Academy of Sciences, Mingsheng Ying Tsinghua University | ||
17:55 - 18:10 | |||
17:55 7mTalk | FM 2026 Closing Main Plenaries / Invited Talks | ||
18:02 7mTalk | FM 2027 Announcement Main Plenaries / Invited Talks | ||