2F Conference Room

VenueHitotsubashi Hall

Room name2F Conference Room

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

	11:15 - 11:30	Industry Day OpeningIndustry Day at 2F Conference Room Chair(s): Naoto Sato Hitachi, Ltd.

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 20m Industry 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 20m Industry talk		(Extended Abstract) Verifiably UX Compliant and User-Intent Layout Generation Industry Day Joana Coutinho OutSystems, Alexandre Lemos OutSystems, Pedro Resende OutSystems
12:10 20m Industry 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

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 20m Industry 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 20m Industry 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 20m Industry 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

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 20m Industry 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 20m Industry 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 20m Industry talk		Pragmatic Uses of AI in Formal Methods–Based Railway Projects: Early Lessons and Perspectives Industry Day Thierry Lecomte CLEARSY, Dalay Almeida CLEARSY, Norman Maury CLEARSY

	17:50 - 18:05	Industry Day ClosingIndustry Day at 2F Conference Room Chair(s): Jeroen Keiren Eindhoven University of Technology, The Netherlands

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

10:40 - 12:30	Session 3: Concurrency & Memory ModelsResearch Track at 2F Conference Room Chair(s): Brijesh Dongol University of Surrey

10:40 25m Talk		Automatic Memory Management for Dataflows Research Track Michael Lienhardt
11:05 25m Talk		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 25m Talk		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 25m Talk		Generating Rely-Guarantee Conditions with the Conditional-Writes Domain Research Track James Tobler The University of Queensland, Graeme Smith The University of Queensland

14:10 - 15:35	TAP Session 2: Program Analysis, Testing & CoverageTAP Track at 2F Conference Room Chair(s): Nikolai Kosmatov Thales Research & Technology

14:10 25m Talk		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 25m Talk		From Execution to Necessity: Proof-Based Metrics for Code Coverage TAP Track Peter Backeman Mälardalen University, Karl Mattson Mälardalen University
15:00 25m Talk		Active Automata Learning with Noisy Data: From Big to Small Data TAP Track Felix Wallner Institute for Formal Models and Verification, Johannes Kepler University Linz, Bernhard Aichernig Johannes Kepler University, Linz, Benjamin von Berg Graz University of Technology, Maximilian Rindler Graz University of Technology

16:05 - 17:55	Session 5: Logic and SemanticsResearch Track at 2F Conference Room Chair(s): Zhenya Zhang Kyushu University

16:05 25m Talk		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 25m Talk		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 25m Talk		Reachability-guided Abstraction Refinement Research Track Pierre Ganty IMDEA Software Institute, Spain, Nicolas Manini IMDEA Software Institute, Francesco Ranzato University of Padova
17:20 25m Talk		Maximum Realizability for LTL Modulo Theories Research Track Andoni Rodríguez IMDEA Software Institute, Spain, César Sánchez IMDEA Software Institute

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

10:40 - 12:20	Session 7: Programming Languages & Program LogicResearch Track at 2F Conference Room Chair(s): Masaki Waga Kyoto University

10:40 25m Talk		RustyDL: A Program Logic for Rust Research Track Daniel Drodt Technical University of Darmstadt, Reiner Hähnle Technical University of Darmstadt DOI
11:05 25m Talk		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 25m Talk		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 25m Talk		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 File Attached

13:50 - 15:30	Session 9: Automata & Reactive ModelsResearch Track at 2F Conference Room Chair(s): Nikolai Kosmatov Thales Research & Technology

13:50 25m Talk		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 25m Talk		Error-awareness Accelerates Active Automata Learning Research Track Loes Kruger Radboud University, Sebastian Junges Radboud University, Jurriaan Rot Radboud University Nijmegen
14:40 25m Talk		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 25m Talk		Specializing anti-unification for interaction models composition via gate connections Research Track Joel Nguetoum CEA, Boutheina Bannour CEA, Pascale Le Gall CentraleSupelec, Erwan Mahe CEA

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 25m Talk		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
16:35 25m Talk		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
17:00 25m Talk		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:25 25m Talk		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

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
2F Conference Room				Industry Day Industry Day Opening			Industry Day Industry Session 1: Automated Synthesis, Optimization, and Certification																																																Industry Day Industry Session 2: Code-Level Verification, Repair, and Testing																Industry Day Industry Session 3: AI-Assisted Requirements Engineering and Early-Stage Analysis												Industry Day Industry Day Closing

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


Room	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 Conference Room									Research Track Session 3: Concurrency & Memory Models																																										TAP Track TAP Session 2: Program Analysis, Testing & Coverage																							Research Track Session 5: Logic and Semantics

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


Room	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 Conference Room									Research Track Session 7: Programming Languages & Program Logic																																						Research Track Session 9: Automata & Reactive Models																												Research Track Session 11: Cyber-Physical & Robotics Systems

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
2F Conference Room							FM Industry Day Efficient Multi-Level Mine Dewatering Using UPPAAL Stratego 11:30 - 11:50				FM Industry Day (Extended Abstract) Verifiably UX Compliant and User-Intent Layout Gene ... 11:50 - 12:10				FM Industry Day Formal Verification for Security Certification: From a First Success to ... 12:10 - 12:30																																								FM Industry Day Formal Verification of Functional Correctness for the OpenHarmony LiteO ... 15:30 - 15:50				FM Industry Day Robustness Semantics based Configuration Bug Fixing for Automated Drivi ... 15:50 - 16:10				FM Industry Day SeaCoral: A Collaborative Test Generation Toolset for Industrial Orches ... 16:10 - 16:30								FM Industry Day Automated ITL Specification Generation from Industrial Aerospace Requir ... 16:50 - 17:10				FM Industry Day Shift-Left Requirements Verification: Integrating LLMs and Formal Metho ... 17:10 - 17:30				FM Industry Day Pragmatic Uses of AI in Formal Methods–Based Railway Projects: Early Le ... 17:30 - 17:50

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


Room	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 Conference Room									FM Research Track Automatic Memory Management for Dataflows 10:40 - 11:05					FM Research Track Complexity of Consistency Testing for the Release-Acquire Semantics 11:05 - 11:30					FM Research Track Towards Proving Liveness on Weak Memory 11:30 - 11:55					FM Research Track Generating Rely-Guarantee Conditions with the Conditional-Writes Domain 11:55 - 12:20																											FM TAP Track Selective Concolic Testing 14:10 - 14:35					FM TAP Track From Execution to Necessity: Proof-Based Metrics for Code Coverage 14:35 - 15:00					FM TAP Track Active Automata Learning with Noisy Data: From Big to Small Data 15:00 - 15:25													FM Research Track A General Framework for Robust Quantitative Semantics of Signal Tempora ... 16:05 - 16:30					FM Research Track Quantitative Monitoring of Signal First-Order Logic 16:30 - 16:55					FM Research Track Reachability-guided Abstraction Refinement 16:55 - 17:20					FM Research Track Maximum Realizability for LTL Modulo Theories 17:20 - 17:45

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


Room	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 Conference Room									FM Research Track RustyDL: A Program Logic for Rust 10:40 - 11:05					FM Research Track Array-Carrying Symbolic Execution for Function Contract Generation 11:05 - 11:30					FM Research Track A Framework for the Interoperable Specification and Verification of Enc ... 11:30 - 11:55					FM Research Track Verifying Sampling Algorithms via Distributional Invariants 11:55 - 12:20																							FM Research Track Asynchronous Team Automata 13:50 - 14:15					FM Research Track Error-awareness Accelerates Active Automata Learning 14:15 - 14:40					FM Research Track Pacing Types for Asynchronous Stream Equations 14:40 - 15:05					FM Research Track Specializing anti-unification for interaction models composition via ga ... 15:05 - 15:30													FM Research Track Exact Moment Estimation of Stochastic Differential Dynamics 16:10 - 16:35					FM Research Track Incremental Synthesis of Safe Controller Guided by Learning-Enabled Bar ... 16:35 - 17:00					FM Research Track Test Coverage of Automated Robotic Systems in Open World Environments 17:00 - 17:25					FM Research Track QSeqSim: A Symbolic Simulator for Qiskit While Loops using Sequential Q ... 17:25 - 17:50

Room information: 2F Conference Room

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

Industry Day

Industry Day

Industry Day

Industry Day

Industry Day

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

Research Track

TAP Track

Research Track

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

Research Track

Research Track

Research Track

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 Conference Room

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

Industry Day

Industry Day

Industry Day

Industry Day

Industry Day

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

Research Track

TAP Track

Research Track

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

Research Track

Research Track

Research Track

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