Portrait of Dr. Ming Fu

Operating systems · Formal verification · Weak memory models

Ming Fu 付明

Director, Huawei Fields Lab · Huawei Technologies Co., Ltd.

I work on reliable and high-performance systems software, with a focus on concurrency verification, weak memory consistency, OS architecture, and formal verification of operating systems and synchronization primitives. My research connects rigorous program reasoning with deployed industrial systems.

Download CV Email libvsync
2023-Present Director of Huawei Fields Lab
2019-2023 Founded and led Huawei Dresden Research Center
ASPLOS 2021 Distinguished Paper Award for VSync
OSDI / SOSP / ASPLOS Systems and verification research at top venues

Research

Verification techniques for real systems

My research agenda is to make formal methods useful for performance-critical systems software. Recent work studies verified synchronization primitives, scalable mobile rendering services, verified memory allocation, efficient tracing, and program migration across weak memory architectures.

Concurrency Verification

Program logics, refinement reasoning, and verification of fine-grained concurrent algorithms.

Weak Memory Models

Verification and optimization of synchronization primitives on Arm and other weak-memory architectures.

Operating Systems

OS architecture, kernel verification, rendering services, tracing, scheduling, and multicore scalability.

Industrial Formal Methods

Building tools and methods that scale from proofs to production systems and open-source libraries.

Systems and Open Source

Research artifacts with practical impact

2021-Present

VSync / libvsync

A verified library of synchronization primitives and concurrent data structures for weak memory architectures. The VSync research line received the ASPLOS 2021 Distinguished Paper Award.

2019-2023

Huawei Dresden Research Center

Founded the research center from scratch while on assignment in Germany, and led a team working on concurrency verification, weak memory consistency, synchronization, and systems software reliability.

2017-2019

Hongmeng OS Kernel Verification

Led formal verification work for key microkernel components and participated in the design and development of the Hongmeng microkernel.

Appointments

Academic and industrial research leadership

2023-Present

Director, Huawei Fields Lab

Huawei Technologies Co., Ltd., Hangzhou, China.

2019-2023

Founder and Director, Huawei Dresden Research Center

Established the center from the ground up and led its research team in Dresden, Germany.

2017-2019

Senior Expert, Huawei OS Kernel Lab

Formal verification and microkernel research for Hongmeng OS.

2011-2017

University of Science and Technology of China

Postdoctoral researcher and associate professor in systems verification.

2009-2010

Visiting Assistant in Research, Yale University

Program logic for optimistic concurrent programs. Advisor: Zhong Shao.

Publications

Selected publications

* denotes corresponding author.

2026

2025

2023

2022-2021

Earlier work

Talks and Service

Public presentations and community leadership

2024

End-to-End Industrial Practice for High-Performance Safe Concurrency

CCF China Software Conference 2024, Formal Methods in Systems Software Forum.