Eric Mullen

I am a graduate student at the University of Washington, in the Programming Languages and Software Engineering group. I am advised by Zachary Tatlock and Dan Grossman. I joined the group in Fall 2012, and will be defending my thesis on May 30, 2018 at 2pm, in room CSE 403.

I care deeply about software correctness. Specifically, I believe that the best path forwards towards software which we can trust and rely on involves building real, formally verified software infrastructure. This belief informs and drives my work. My first project in grad school was Peek, a verified peephole optimizer for CompCert. My current research is the Oeuf project, a verified extraction mechanism for Coq.

I have a rather unusual diet due to an overgrowth of bacteria in my small intestine, or SIBO. For more details on what I eat go here

In order to reach me, simply send me an email at:


J. Dodds, A. Chudnov, A. Tomb, S. Magill, N. Collins, E. Westbrook, B. Cook, S. Tasiran, C. MacCarthaigh, E. Mertens, E. Mullen, and B. Huffman. Continuous formal verification of Amazon s2n. CAV'18.

R. Kumar, E. Mullen, Z. Tatlock, and M. O. Myreen. Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (short paper). ITP'18.

E. Mullen, S. Pernsteiner, J. R. Wilcox, Z. Tatlock, and D. Grossman. Oeuf: Minimizing the Coq Extraction TCB. CPP’18.

E. Mullen, D. Zuniga, Z. Tatlock, and D. Grossman. Verified Peephole Optimizations for CompCert. PLDI'16.