Dr. Ming Fu

Selected Publications

2025

• StereoFG: Generating Stereo Frames from Centered Feature Stream
  Chenyu Zuo, Yazhen Yuan, Zhizhen Wu, Zhijian Liu, Jingzhen Lan, Ming Fu, Yuchi Huo, Rui Wang
  SIGGRAPH Asia 2025, December 16–18, 2025
• OS Rendering Service Made Parallel with Out-of-Order Execution and In-Order Commit
  Yuanpei Wu, Dong Du, Chao Xu, Yubin Xia, Yang Yu, Ming Fu, Binyu Zang, Haibo Chen
  OSDI 2025, July 7–9, 2025
• D-VSync: Decoupled Rendering and Displaying for Smartphone Graphics
  Yuanpei Wu, Dong Du, Chao Xu, Yubin Xia, Ming Fu, Binyu Zang, Haibo Chen
  ASPLOS 2025, March 2025
• Enabling Efficient Mobile Tracing with BTrace
  Jiawei Wang, Nian Liu, Arnau Casadevall-Saiz, Yutao Liu, Diogo Behrens, Ming Fu, Ning Jia, Hermann Härtig, Haibo Chen
  ASPLOS 2025, March 2025

2023

• BWoS: Formally Verified Block-based Work Stealing for Parallel Processing
  Jiawei Wang, Bohdan Trach, Ming Fu*, Diogo Behrens, Jonathan Schwender, Yutao Liu, Jitang Lei, Viktor Vafeiadis, Hermann Härtig, Haibo Chen
  OSDI 2023, July 10–12, 2023
  Slides
• AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMM
  Martin Beck, Koustubha Bhat, Lazar Stričević, Geng Chen, Diogo Behrens, Ming Fu*, Viktor Vafeiadis, Haibo Chen, Hermann Härtig
  ASPLOS 2023, March 2023

2022

• BBQ: A Block-based Bounded Queue for Exchanging Data and Profiling
  Jiawei Wang, Diogo Behrens, Ming Fu*, Lilith Oberhauser, Jonas Oberhauser, Jitang Lei, Geng Chen, Hermann Härtig, Haibo Chen
  USENIX ATC 2022, July 11–13, 2022
• Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models
  Antonio Paolillo, Hernán Ponce-de-León, Thomas Haas, Diogo Behrens, Rafael Chehab, Ming Fu, Roland Meyer
  Technical Note, arXiv, July 9, 2022

2021

• CLoF: A Compositional Lock Framework for Multi-level NUMA Systems
  Rafael Lourenco de Lima Chehab, Antonio Paolillo, Diogo Behrens, Ming Fu*, Hermann Härtig, Haibo Chen
  SOSP 2021, October 25-28, 2021
• Verifying and Optimizing the HMCS Lock for Arm Servers
  Jonas Oberhauser, Lilith Oberhauser, Antonio Paolillo, Diogo Behrens, Ming Fu, Viktor Vafeiadis
  NETYS 2021, May 2021
• VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models Distinguished Paper
  Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu*, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, Viktor Vafeiadis
  ASPLOS 2021, April 2021
  Short Talk Full Talk

2020

• Formalizing SPARCv8 Instruction Set Architecture in Coq
  Jiawei Wang, Ming Fu, Lei Qiao, Xinyu Feng
  Science of Computer Programming, 187: 102371, 2020

2019

• Using Concurrent Relational Logic with Helper for Verifying the AtomFS File System
  Mo Zou, Haoran Ding, Dong Du, Ming Fu, Ronghui Gu, Haibo Chen
  SOSP 2019, October 27-30, 2019

2016

• A Practical Verification Framework for Preemptive OS Kernels
  Fengwei Xu, Ming Fu*, Xinyu Feng, Xiaoran Zhang, Hui Zhang, Zhaohui Li
  CAV 2016, July 2016

2015

• Practical Tactics for Verifying C Programs in Coq
  Jingyuan Cao, Ming Fu*, Xinyu Feng
  CPP 2015, January 2015

2014

• Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations
  Hongjin Liang, Xinyu Feng, Ming Fu
  ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 36, No. 1, Article 3, March 2014

2013

• Applying Mathematical Logic to Create Zero-Defect Software
  Yanni Kouskoulas, Ming Fu, Zhong Shao, Peter Kazanzides
  Johns Hopkins APL Technical Digest, Volume 32, Number 2, 2013

2012

• A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations
  Hongjin Liang, Xinyu Feng, Ming Fu
  POPL 2012, January 2012

2010

• Reasoning about Optimistic Concurrency Using a Program Logic for History
  Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, Yu Zhang
  CONCUR 2010, August 2010