Eric Mullen

I currently work for Google, on the Asylo project.

I graduated from the University of Washington, in the Programming Languages and Software Engineering group in 2018. I was (and still am) advised by Zachary Tatlock and Dan Grossman. I joined the group in Fall 2012.

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

I am an ordained minister in the Church of the Flying Spaghetti Monster

In order to reach me, simply send me an email at: emullen@cs.washington.edu.

Publications

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.