Formal Verification of Functional Correctness for the OpenHarmony LiteOS-M Kernel (FM 2026 - Industry Day)

Who

Tianqi Zhao, Qinxiang Cao, Shenghua Feng, Minghui Zhou, Naijun Zhan, Yongzhi Cao, Junfeng Zhao, Haiyan Zhao, Hao Wang, Zhenjiang Hu

Track

FM 2026 Industry Day

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

When

Wed 20 May 2026 15:30 - 15:50 at 2F Conference Room - Industry Session 2: Code-Level Verification, Repair, and Testing Chair(s): Cristina Seceleanu

Tianqi Zhao

Zhongguancun Laboratory

China

Qinxiang Cao

Shanghai Jiao Tong University

China

Shenghua Feng

Zhongguancun Laboratory

China

Minghui Zhou

Peking University

China

Naijun Zhan

Peking University; Zhongguancun Laboratory

China

Yongzhi Cao

Peking University

China

Junfeng Zhao

Inner Mongolia University

Haiyan Zhao

Peking University

China

Hao Wang

Shenzhen Kaihong Digital Industry Development Co., Ltd.

China

Zhenjiang Hu

Peking University

China

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

Display full programSpecify a time band

Save

Session Program

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

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