Alex Sanchez-Stern
Hey I’m Alex Sanchez-Stern, I’m a Postdoctoral researcher at UMass
Amherst. I graduated from the University of Washington with a Masters
degree in the Spring of 2016, and finished my PhD at UC San Diego in
the Spring of 2021. I’m also part of the team at the UW that built
Herbie. I’m generally interested in using
programming language techniques to bring hard-fought domain expertise
to more everyday programmers. My PhD thesis was on
Proverbot9001, a neural-guided proof
search tool described on the projects page, and in the MAPL paper below. Since then, I’ve
been working on a few different tools in the space of proof synthesis.
I taught
CSE333 at
the University of Washington in the Summer of 2024.
Publications
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
[paper]
[github]
Alex Sanchez-Stern, Abhishek Varghese, Zhanna Kaufman, Dylan Zhang Talia Ringer, Yuriy Brun
ICSE 2025
Passport: Improving Automated Formal Verification with Identifiers
[paper]
[github]
[talk video]
Alex Sanchez-Stern, Emily First, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, and Talia Ringer
TOPLAS 2023
Proofster: Automated Formal Verification
[paper]
[github]
[website]
Arpan Agrawal, Emily First, Zhanna Kaufman, Tom Reichel, Shizhou Zhang, Timothy Zhou, Alex Sanchez-Stern, Talia Ringer, Yuriy Brun
ICSE 2023 Demo Track
Data-Driven Lemma Synthesis for Interactive Proofs
[paper]
[artifact]
Aishwarya Sivaraman, Alex Sanchez-Stern, Bretton Chen, Sorin Lerner, Todd Millstein
OOPSLA 2022
Scooter & Sidecar: A Domain-Specific Approach to Writing Secure Migrations
[paper]
John Renner, Alex Sanchez-Stern, Fraser Brown, Sorin Lerner, Deian Stefan
PLDI 2021
Generating Correctness Proofs with Neural Networks
[paper]
[website]
[talk video]
Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, Sorin Lerner
MAPL 2020
REPLica: REPL instrumentation for Coq Analysis
[paper]
[github]
Talia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner
CPP 2020
Finding Root Causes of Floating Point Error
[paper]
[website]
Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock
PLDI 2018
Towards a Standard Benchmark Format and Suite for Floating-Point Analysis
[paper]
[website]
Nasrine Damouche, Matthieu Martel, Pavel Panchekha, Jason Qiu, Alex Sanchez-Stern, Zachary Tatlock
NSV 2016
Automatically Improving Accuracy for Floating-Point Expressions
[paper]
[website]
Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, Zachary Tatlock
PLDI 2015 (Distinguished Paper Award)
You can reach me at alex.sanchezstern@gmail.com. I’m
also on GitHub.