Haobin Ni
Ph.D. Candidate, Cornell University
haobin [at]

I am a sixth-year Ph.D. student at Cornell University, co-advised by Greg Morrisett and Robbert van Renesse. My research focuses on formal verification of practical systems, primarily distributed systems. I believe in both principled theories and practical implementation and aim to bring together the best of both worlds through thoughtful designs. So I am also broadly interested in projects in the broader programming language and system scope. I have collaborated on projects that involve domain-specific languages, consensus protocols, information flow control, and language-based security.

As a competitive programming veteran who won a silver and a gold at the 2014 and 2016 ICPC World Finals, I have been coaching the Cornell ICPC team since 2018. I also volunteered as a problem-setter and judge in the Cornell High School Programming Contest. My Codeforces ID is TankEngineer.

Besides doing research and competitive programming, I enjoy good humor, cooking various food, and having my dose of existential doubts.


ASN1★: Provably Correct Non-Malleable Parsing for ASN.1 DER, To appear in CPP '23
Haobin Ni , Antoine Delignat-Lavaud , Cédric Fournet , Tahina Ramananandro , Nikhil Swamy
Hardening attack surfaces with formally proven binary format parsers, PLDI '22
Nikhil Swamy , Tahina Ramananandro , Aseem Rastogi , Irina Spiridonova , Haobin Ni , Dmitry Malloy , Juan Vazquez , Michael Tang , Omar Cardona , Arti Gupta
Compositional security for reentrant applications, IEEE S&P '21 Best Paper Award
Ethan Cecchetti , Siqiu Yao , Haobin Ni , Andrew C Myers