1F Room 101-103

VenueHitotsubashi Hall

Room name1F Room 101-103

Floor1

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

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

09:15 - 10:40	AIPV Day 1 Session 1 VerificationWorkshop: AIPV at 1F Room 101-103

09:15 5m Day opening		AIPV Day 1 Opening Workshop: AIPV
09:20 40m Keynote		AIPV Keynote: Conrad Watt Workshop: AIPV Conrad Watt Nanyang Technological University
10:00 20m Talk		Machine Learning for Stream-Based Diagnosis Workshop: AIPV Raik Hipler University of Lübeck, Martin Leucker University of Lübeck
10:20 20m Talk		A Minimal Agent for Automated Theorem Proving Workshop: AIPV Borja Requena Axiomatic AI, Austin Letson Axiomatic AI, Krystian Nowakowski Axiomatic AI, Izan Beltran Ferreiro Axiomatic AI, Leopoldo Sarra Axiomatic AI

11:00 - 12:40	AIPV Day 1 Session 2 Isabelle & RocqWorkshop: AIPV at 1F Room 101-103

11:00 20m Talk		Automated Sketching and Repairing of Large Mechanised Proofs Workshop: AIPV Chengsong Tan Kaihong, Jonathan Julian Huerta y Munive Aalborg University in Copenhagen, John Wickerson Imperial College London, Alastair F. Donaldson Imperial College London
11:20 20m Talk		Inverting the Formalization Workflow: Prototyping an MPC Protocol in Rocq with an LLM Agent Workshop: AIPV Cheng-Hui Weng Nagoya University
11:40 20m Talk		Formalizing Actuarial Mathematics in Proof Assistants Workshop: AIPV Yosuke Ito Sompo Himawari Life Insurance Inc.
12:00 20m Talk		A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL Workshop: AIPV Qiyuan Xu Nanyang Technological University, Renxi Wang MBZUAI, Peixin Wang East China Normal University, Haonan Li MBZUAI, Conrad Watt Nanyang Technological University
12:20 20m Talk		Sponsor Talk by Harmonic: Automatically Formally Verified Software using Aristotle Workshop: AIPV

14:00 - 15:30	AIPV Day 1 Session 3 MathematicsWorkshop: AIPV at 1F Room 101-103

14:00 40m Keynote		AIPV Keynote: Autoformalization Across Proof Assistants: Languages, Proof Styles, and Automation Workshop: AIPV Cezary Kaliszyk University of Melbourne
14:40 20m Talk		Toward Textbook-Scale Autoformalization with Large Language Models Workshop: AIPV Hyojae Lim Korea Institute for Advanced Study (KIAS)
15:00 20m Talk		Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs Workshop: AIPV Kaito Baba The University of Tokyo, Chaoran Liu Research and Development Center for Large Language Models,National Institute of Informatics, Shuhei Kurita National Institute of Informatics, Akiyoshi Sannai Kyoto University

16:00 - 17:30	AIPV Day 1 Session 4 ApplicationWorkshop: AIPV at 1F Room 101-103

16:00 20m Talk		Sponsor Talk by Hendrik Skubch, Noeon Research: Towards Trustable Machine Reasoning - A case study using variant Sudoku Workshop: AIPV
16:20 20m Talk		Validating Formal Specifications with LLM-generated Test Cases Workshop: AIPV Alcino Cunha University of Minho; INESC TEC, Nuno Macedo University of Porto; INESC TEC File Attached
16:40 40m Other		AIPV Workshop Session Workshop: AIPV

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

09:00 - 10:30	AIPV Day 2 Session 1 TheoryWorkshop: AIPV at 1F Room 101-103

09:00 22m Day opening		AIPV Day 2 Opening Workshop: AIPV
09:22 22m Keynote		AIPV Keynote: Nobuko Yoshida, Resilient Distributed Intelligent Swarms and Safeguarded AI: Programming Models and Runtime Guarantees Workshop: AIPV Nobuko Yoshida University of Oxford, UK
09:45 22m Talk		Neural Continuous-Time Supermartingale Certificates Workshop: AIPV Grigory Neustroev Zeroth Research, Mirco Giacobbe University of Birmingham, Anna Lukina Delft University of Technology
10:07 22m Talk		From Behaviour-Driven Development Scenarios to Formally Verifiable Behavioural Models via Dynamic Condition Response Graphs Workshop: AIPV Xinyuan Tu University of Copenhagen, Thomas T. Hildebrandt University of Copenhagen, Thiago Rocha Silva University of Southern Denmark

11:00 - 12:20	AIPV Day 2 Session 2 LeanWorkshop: AIPV at 1F Room 101-103

11:00 20m Talk		Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium Workshop: AIPV Vasily Ilin Axiom Math Pre-print
11:20 20m Talk		Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization Workshop: AIPV Banri Yanahama Nyx Foundation, Akiyoshi Sannai Kyoto University Pre-print
11:40 20m Talk		SorryDB: Can AI Provers Complete Real-World Lean Theorems? Workshop: AIPV Austin Letson Axiomatic AI, Leopoldo Sarra Axiomatic AI, Auguste Poiroux Math, Inc; EPFL, Oliver Dressler --, Paul Lezeau Imperial College; The London School of Geometry and NumberTheory, Dhyan Aranha University of Amsterdam; Cote d'Azur University, Frederik Pu University of Toronto, Aaron Hill ---, Miguel Corredera Hidalgo ENSEIRB-MATMECA, INP-Bordeaux, Julian Berman Columbia University, George Tsoukalas The University of Texas at Austin, Lenny Taelman University of Amsterdam
12:00 20m Talk		Sponsor Talk by Jimmy Shin, AxiomMath.ai: AXLE: Free, Public Lean 4 Tooling for AI-Driven Mathematics Workshop: AIPV

14:00 - 15:20	AIPV Day 2 Session 3 Neural NetworkWorkshop: AIPV at 1F Room 101-103

14:00 20m Talk		s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs Workshop: AIPV Balaji Rao Stevens Institute of Technology, John Harrison Amazon Web Services, Soonho Kong Amazon Web Services, Juneyoung Lee AWS, Carlo Lipizzi Stevens Institute on Technology
14:20 20m Talk		Exact Verification of Graph Neural Networks with Incremental Constraint Solving Workshop: AIPV Minghao Liu University of Oxford, Chia-Hsuan Lu University of Oxford, Marta Kwiatkowska University of Oxford
14:40 20m Talk		Formal Reasoning About Confidence and Automated Verification of Neural Networks Workshop: AIPV 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
15:00 20m Talk		Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models Workshop: AIPV Sho Sonoda RIKEN / CyberAgent

16:00 - 17:50	AIPV Day 2 Session 4 LLMWorkshop: AIPV at 1F Room 101-103

16:00 20m Talk		Large Language Models for Verification of Reactive Programs Workshop: AIPV Holly Hendry University of York, Pedro Ribeiro University of York, UK, Frank Soboczenski University of York, Kings College London, Alan TuringInstitute
16:20 20m Talk		Towards an Agentic LLM-based Approach to Requirement Formalization from Unstructured Specifications Workshop: AIPV Alberto Tagliaferro Politecnico di Milano, Italy, Bruno Guindani Politecnico di Milano, Livia Lestingi DEIB, Politecnico di Milano, Matteo Rossi Politecnico di Milano
16:40 20m Talk		Signal Shot: End-to-End Formal Verification of Signal’s Cryptographic Stack Workshop: AIPV
17:00 40m Panel		AIPV Panel Discussion Workshop: AIPV
17:40 10m Day closing		AIPV Closing Workshop: AIPV

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

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 - ABZ Dominique Mery Université de Lorraine, CNRS, INRIA / LORIA & Telecom Nancy, France

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 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 25m Talk		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 15m Talk		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

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 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 25m Talk		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 25m Talk		A Spectabular Model of an Automotive Adaptive Exterior Light System ABZ 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 ABZ

Mon 18 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
1F Room 101-103				Workshop: AIPV AIPV Day 1 Session 1 Verification																					Workshop: AIPV AIPV Day 1 Session 2 Isabelle & Rocq																																				Workshop: AIPV AIPV Day 1 Session 3 Mathematics																								Workshop: AIPV AIPV Day 1 Session 4 Application

Tue 19 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
1F Room 101-103	Workshop: AIPV AIPV Day 2 Session 1 Theory																								Workshop: AIPV AIPV Day 2 Session 2 Lean																																				Workshop: AIPV AIPV Day 2 Session 3 Neural Network																								Workshop: AIPV AIPV Day 2 Session 4 LLM

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


Room	11:00						30						12:00						30						13:00						30						14:00						30						15:00						30						16:00						30						17:00						30						18:00						30
1F Room 101-103				ABZ ABZ Invited Talk 3: Dominique Mery												ABZ																																							ABZ ABZ Session 5: Methods (2)															ABZ ABZ Session 6: Case Study															ABZ ABZ Award and Closing

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
1F Room 101-103	Services

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
1F Room 101-103	Services

Mon 18 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
1F Room 101-103				FM Workshop: AIPV AIPV Day 1 Opening 09:15 - 09:20	FM Workshop: AIPV AIPV Keynote: Conrad Watt 09:20 - 10:00								FM Workshop: AIPV Machine Learning for Stream-Based Diagnosis 10:00 - 10:20				FM Workshop: AIPV A Minimal Agent for Automated Theorem Proving 10:20 - 10:40								FM Workshop: AIPV Automated Sketching and Repairing of Large Mechanised Proofs 11:00 - 11:20				FM Workshop: AIPV Inverting the Formalization Workflow: Prototyping an MPC Protocol in Ro ... 11:20 - 11:40				FM Workshop: AIPV Formalizing Actuarial Mathematics in Proof Assistants 11:40 - 12:00				FM Workshop: AIPV A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL 12:00 - 12:20				FM Workshop: AIPV Sponsor Talk by Harmonic: Automatically Formally Verified Software usin ... 12:20 - 12:40																				FM Workshop: AIPV AIPV Keynote: Autoformalization Across Proof Assistants: Languages, Pro ... 14:00 - 14:40								FM Workshop: AIPV Toward Textbook-Scale Autoformalization with Large Language Models 14:40 - 15:00				FM Workshop: AIPV Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs 15:00 - 15:20												FM Workshop: AIPV Sponsor Talk by Hendrik Skubch, Noeon Research: Towards Trustable Machi ... 16:00 - 16:20				FM Workshop: AIPV Validating Formal Specifications with LLM-generated Test Cases 16:20 - 16:40				FM Workshop: AIPV AIPV Workshop Session 16:40 - 17:20

Tue 19 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
1F Room 101-103	FM Workshop: AIPV AIPV Day 2 Opening 09:00 - 09:22				FM Workshop: AIPV AIPV Keynote: Nobuko Yoshida, Resilient Distributed Intelligent Swarms ... 09:22 - 09:45					FM Workshop: AIPV Neural Continuous-Time Supermartingale Certificates 09:45 - 10:07				FM Workshop: AIPV From Behaviour-Driven Development Scenarios to Formally Verifiable Beha ... 10:07 - 10:30											FM Workshop: AIPV Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium 11:00 - 11:20				FM Workshop: AIPV Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Colla ... 11:20 - 11:40				FM Workshop: AIPV SorryDB: Can AI Provers Complete Real-World Lean Theorems? 11:40 - 12:00				FM Workshop: AIPV Sponsor Talk by Jimmy Shin, AxiomMath.ai: AXLE: Free, Public Lean 4 Too ... 12:00 - 12:20																								FM Workshop: AIPV s2n-bignum-bench: A practical benchmark for evaluating low-level code r ... 14:00 - 14:20				FM Workshop: AIPV Exact Verification of Graph Neural Networks with Incremental Constraint ... 14:20 - 14:40				FM Workshop: AIPV Formal Reasoning About Confidence and Automated Verification of Neural ... 14:40 - 15:00				FM Workshop: AIPV Why Agentic Theorem Prover Works: A Statistical Provability Theory of M ... 15:00 - 15:20												FM Workshop: AIPV Large Language Models for Verification of Reactive Programs 16:00 - 16:20				FM Workshop: AIPV Towards an Agentic LLM-based Approach to Requirement Formalization from ... 16:20 - 16:40				FM Workshop: AIPV Signal Shot: End-to-End Formal Verification of Signal’s Cryptographic Stack 16:40 - 17:00				FM Workshop: AIPV AIPV Panel Discussion 17:00 - 17:40								FM Workshop: AIPV AIPV Closing 17:40 - 17:50

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


Room	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
1F Room 101-103				FM ABZ Systematic Development of Distributed Algorithms using Event-B - Experi ... 11:15 - 12:15																																																			FM ABZ Counterexample-Guided Interval Weakening 15:30 - 15:55					FM ABZ Specification and Analysis of Ethical Requirements in Autonomous System ... 15:55 - 16:20					FM ABZ Evaluating the Practical Impact of Parallelism in Asmeta 16:20 - 16:35					FM ABZ Formal Modeling and Analysis of a Planetary Rover under Abnormal Scenar ... 16:45 - 17:10					FM ABZ Can Large Language Models Support Modeling Systems with ASMETA? A Case ... 17:10 - 17:35					FM ABZ A Spectabular Model of an Automotive Adaptive Exterior Light System 17:35 - 18:00					FM ABZ ABZ Award and Closing 18:00 - 18:10

Room information: 1F Room 101-103

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

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

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

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

Workshop: AIPV

Workshop: AIPV

Workshop: AIPV

Workshop: AIPV

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

Workshop: AIPV

Workshop: AIPV

Workshop: AIPV

Workshop: AIPV

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

ABZ

ABZ

ABZ

ABZ

ABZ

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

Services

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

Services

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

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

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

Tracks

Room information: 1F Room 101-103

Program Display Configuration

Mon 18 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

Tue 19 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

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

Mon 18 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

Workshop: AIPV

Workshop: AIPV

Workshop: AIPV

Workshop: AIPV

Tue 19 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

Workshop: AIPV

Workshop: AIPV

Workshop: AIPV

Workshop: AIPV

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

ABZ

ABZ

ABZ

ABZ

ABZ

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

Services

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

Services

Mon 18 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

Tue 19 MayDisplayed time zone: Osaka, Sapporo, Tokyo change

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

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

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

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

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

Tue 19 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

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

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

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