Ming Fu 付明

Chief Expert, Huawei Fields Lab

Shanghai, China · since July 2026

ming.fu@huawei.com

Ming Fu

I work on operating systems and formal verification. My research focuses on concurrent programs, synchronization, and weak memory models.

Recent work includes verified memory allocation and work stealing, as well as parallel rendering and tracing on mobile devices. Some of our work on synchronization is available in libvsync.

Selected publications

* denotes corresponding author.

2026

2025

2023

2022-2021

Earlier work

Software

libvsync

A library of verified synchronization primitives and concurrent data structures for weak memory architectures. Related to our VSync paper at ASPLOS 2021.

CertiuCOS2

A framework for proving that preemptive kernel implementations refine their abstract specifications, with a uC/OS-II case study. The code now builds with Rocq 9.2. The README covers the build, proof scope, and known assumptions. Research materials.

Experience

  1. –present

    Chief Expert, Huawei Fields Lab

    Huawei Technologies Co., Ltd. · Shanghai, China

  2. Aug 2023–Jun 2026

    Director, Huawei Fields Lab

    Huawei Technologies Co., Ltd. · Hangzhou, China

  3. 2019–2023

    Founder and Director, Huawei Dresden Research Center

    Established and led the research center in Dresden, Germany.

  4. 2017–2019

    Senior Expert, Huawei OS Kernel Lab

    Formal verification and microkernel research for Hongmeng OS.

  5. 2011–2017

    University of Science and Technology of China

    Postdoctoral researcher and associate professor in systems verification.

  6. 2009–2010

    Visiting Assistant in Research, Yale University

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

Talks and service