Publications

Full-length Publications

Robert Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez-Stern, Yuriy Brun, João F. Ferreira, Sorin Lerner, Emily First
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
ICSE 2025
ACM SIGSOFT Distinguished Paper Award

Chenyang An, Zhibo Chen, Qihao Ye, Emily First, Letian Peng, Jiayun Zhang, Zihan Wang, Sorin Lerner, Jingbo Shang
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving
ACL Main 2024

Emily First, Markus N. Rabe, Talia Ringer, Yuriy Brun
Baldur: Whole-Proof Generation and Repair with Large Language Models
ESEC/FSE 2023
ACM SIGSOFT Distinguished Paper Award

Alex Sanchez-Stern*, Emily First*, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, Talia Ringer
Passport: Improving Automated Formal Verification Using Identifiers
(*Co-first authors)
TOPLAS 2023
(Presented as a journal-first paper at PLDI 2023)

Emily First, Yuriy Brun
Diversity-Driven Automated Formal Verification
ICSE 2022
ACM SIGSOFT Distinguished Paper Award

Emily First, Yuriy Brun, Arjun Guha.
TacTok: Semantics-Aware Proof Synthesis
OOPSLA 2020

Preprints

Yousef Alhessi, Sólrún Halla Einarsdóttir, George Granberry, Emily First, Moa Johansson, Sorin Lerner, Nicholas Smallbone
Lemmanaid: Neuro-Symbolic Lemma Conjecturing
arXiv 2025
Under Submission

Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, Emily First
Cobblestone: Iterative Automation for Formal Verification
arXiv 2024
Under Submission

Demo-Track Publications

Pedro Carrott, Nuno Saavedra, Kyle Thompson, Sorin Lerner, João F. Ferreira, Emily First
CoqPyt: Proof Navigation in Python in the Era of LLMs
FSE 2024

Arpan Agrawal, Emily First, Zhanna Kaufman, Tom Reichel, Shizhuo Zhang, Timothy Zhou, Alex Sanchez-Stern, Talia Ringer, Yuriy Brun.
Proofster: Automated Formal Verification
ICSE 2023

Workshop Publications

Sólrún Einarsdóttir, Yousef Alhessi, Emily First, Moa Johansson
On Lemma Conjecturing using Neural, Symbolic and Neuro-symbolic approaches
In 9th Conference on Artificial Intelligence and Theorem Proving
AITP 2024

Shizhuo Dylan Zhang, Emily First, Talia Ringer
Getting More out of Large Language Models for Proofs
In 8th Conference on Artificial Intelligence and Theorem Proving
AITP 2023