Fengmin (Paul) Zhu
Doctoral Student MPI-SWS (PLV)
Have fun with Coq & Cocktails

I’m in my first year of PhD (adviser Derek Dreyer) in MPI-SWS, making investigations on proof-assistant-based formal verification of programs, in particular using Coq and Iris. I received my bachelor and master (adviser Fei He) both in Tsinghua University, where my research focus was on program synthesis and software merging. I enjoy cocktails, an art of mixing various components in a balanced and innovative way, just like inventing exciting new features for a programming language.

NOTE: this page is a more “casual” introduction of me and includes outcomes since undergraduate. It is under construction and some contents will be extended.

Interested Topics

  • Type systems
  • Formal semantics
  • Proof assistants
  • Program synthesis
  • Probabilistic programming
  • Repository mining & merge
  • Compiler construction


  • Bachelor in Computer Science & Technology, Tsinghua University, 2017
  • Master of Software Engineering, Tsinghua University, 2020

Teaching Assistant

  • 30240382 Principles of Compilation, 2017 Fall
  • 30240243 Operating Systems, 2018 Spring
  • 30240382 Principles of Compilation, 2018 Fall
  • 34100352 Functional Programming, 2019 Spring
  • 44100484 Modeling and Verification of Software Systems I, 2019 Spring
  • 30240382 Principles of Compilation, 2019 Fall
  • 44100603 Software Analysis and Verification, 2020 Spring

All the above were at Tsinghua University.


  • Fengmin Zhu, Fei He. Conflict Resolution for Structured Merge via Version Space Algebra. OOPSLA'18. DOI: https://doi.org/10.1145/3276536. Project website
  • Fengmin Zhu, Fei He, Qianshan Yu. Enhancing Precision of Structured Merge by Proper Tree Matching. ICSE'19 Poster.

Selected Projects

  • Decaf project: A simple education-purpose programming language for compiler courses
  • LL1-Parser-Gen: An LL(1) parser generator in principle. (Used in the compilation course)
  • Mastery: A more reasonable and neat three-way structured merge tool (now just for Java).
  • ThuThesis-Starter: A starter template for new users of ThuThesis.
  • Sudoku-BMC: A sudoku solver based upon NuSMV bounded model checker. (course project)
  • LustreAST: A small tool to translate between the Lustre language and its AST representation. (course project)
  • mydb: A simple one-user single-thread database. (course project)

Projects in MPI-SWS that I will work on and possibly contribute to in future:

Selected Talks

Most of them were given in Chinese. Tunight is a traditional event held by TUNA.

Selected Cocktails

Negroni is one of my favorite cocktail and I tried plenty of variants (even one with Jägermeister). I have a telegram channel on cocktail making, though some of the comments are in Chinese.


Email: paulzhu at mpi-sws dot org