Emily First
About me
I am a postdoctoral researcher at UC San Diego working with Sorin Lerner (but I work remotely from NYC). In May 2023, I completed my PhD in Computer Science at UMass Amherst, where I worked with Yuriy Brun in the Laboratory for Software Engineering Research (LASER). My research is at the intersection of software engineering, programming languages, and machine learning. Specifically, I focus on creating tools to automatically generate proofs of software correctness in Coq and Isabelle/HOL. In May 2017, I received a BS in Math and Computer Science from Harvey Mudd College.
Research and Publications
Getting More out of Large Language Models for Proofs
Shizhuo Dylan Zhang, Emily First, Talia Ringer
To appear at AITP 2023
arXiv
Baldur: Whole-Proof Generation and Repair with Large Language Models
Emily First, Markus N. Rabe, Talia Ringer, Yuriy Brun
To appear at ESEC/FSE 2023
arXiv
Passport: Improving Automated Formal Verification Using Identifiers
Alex Sanchez-Stern*, Emily First*, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, Talia Ringer
TOPLAS 2023 (presented at PLDI 2023)
arXiv github (* Co-first authors)
Proofster: Automated Formal Verification
Arpan Agrawal, Emily First, Zhanna Kaufman, Tom Reichel, Shizhuo Zhang, Timothy Zhou, Alex Sanchez-Stern, Talia Ringer, Yuriy Brun
ICSE 2023 (demo track)
preprint, tool
Diversity-Driven Automated Formal Verification
Emily First, Yuriy Brun
ICSE 2022
ACM SIGSOFT Distinguished Paper Award
video, doi, github, VM
TacTok: Semantics-Aware Proof Synthesis
Emily First, Yuriy Brun, Arjun Guha
OOPSLA 2020
video, doi, github, VM