Alex Sanchez-Stern

Alex Sanchez-Stern

Hey I’m Alex Sanchez-Stern, I’m a Senior Research Scientist at dmodel. I did a postdoc 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 spent a few years at UMass Amherst working on various types of machine learning for theorem proving. 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, and I’ll be teaching it again the Summer of 2025.

Publications

Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

[paper] [github]

Robert Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez-Stern, Yuriy Brun, João F. Ferreira, Sorin Lerner, Emily First
ICSE 2025 (Distinguished Paper Award)
@inproceedings{thompson25rango,
   author = {Thompson, Robert and Saavedra, Nuno and Carrot, Pedro, and Fisher, Kevin and Sanchez-Stern, Alex and Brun, Yuriy and Ferreira, João F. and Lerner, Sorin and First, Emily}
   title = {Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification}
   booktitle = {International Conference on Software Engineering}
   month = {April}
   year = {2025}
   publisher = {ACM SIGSOFT}
}

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
@inproceedings{sanchezstern25qedcartographer,
   author = {Sanchez-Stern, Alex and Varghese, Abhishek and Kaufman, Zhanna and Zhang, Dylan and Ringer, Talia and Brun, Yuriy}
   title = {QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning}
   booktitle = {International Conference on Software Engineering}
   month = {April}
   year = {2025}
   publisher = {ACM SIGSOFT}
}

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
@inproceedings{sanchezstern:2023:passport,
  author    = {Sanchez-Stern, Alex and First, Emily and Zhou, Timothy and Kaufman, Zhanna and Brun, Yuriy and Ringer, Talia},
  title     = {Passport: Improving Automated Formal Verification with Identifiers},
  booktitle = {Transactions On Programming Languages And Systems},
  month     = {December},
  year      = {2023},
  publisher = {ACM SIGPLAN},
}

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
@inproceedings{agrawal:2023:proofster,
  author    = {Agrawal, Arpan and First, Emily and Kaufman, Zhanna and Reichel, Tom and Zhang, Shizhou and Zhou, Timothy and Sanchez-Stern, Alex and Ringer, Talia and Brun, Yuriy},
  title     = {Proofster: Automated Formal Verification},
  booktitle = {International Conference on Software Engineering Demonstrations Track},
  month     = {May},
  year      = {2023},
  publisher = {ACM SIGPLAN},
}

Data-Driven Lemma Synthesis for Interactive Proofs

[paper] [artifact]

Aishwarya Sivaraman, Alex Sanchez-Stern, Bretton Chen, Sorin Lerner, Todd Millstein
OOPSLA 2022
@inproceedings{sivaraman:2022:lfind,
  author    = {Sivaraman, Aishwarya and Sanchez-Stern, Alex and Chen, Bretton and Lerner, Sorin and Millstein Todd},
  title     = {Data-Driven Lemma Synthesis for Interactive Proofs},
  booktitle = {Object-Oriented Programming, Systems, Languages & Applications},
  month     = {December},
  year      = {2022},
  publisher = {ACM SIGPLAN},
}

Scooter & Sidecar: A Domain-Specific Approach to Writing Secure Migrations

[paper]

John Renner, Alex Sanchez-Stern, Fraser Brown, Sorin Lerner, Deian Stefan
PLDI 2021
@inproceedings{renner:2021:scooterandsidecar,
  author    = {Renner, John and Sanchez-Stern, Alex and Brown, Fraser and Lerner, Sorin and Stefan, Deian},
  title     = {Scooter & Sidecar: A Domain-Specific Approach to Writing Secure Migrations},
  booktitle = {Programming Languages Design and Implementation},
  month     = {June},
  year      = {2021},
  publisher = {ACM SIGPLAN},
}

Generating Correctness Proofs with Neural Networks

[paper] [website] [talk video]

Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, Sorin Lerner
MAPL 2020
@inproceedings{sanchezstern:2020:proverbot9001,
  author    = {Sanchez-Stern, Alex and Alhessi, Yousef and Saul, Lawrence and Lerner, Sorin},
  title     = {Generating Correctness Proofs with Neural Networks},
  booktitle = {Machine Learning in Programming Languages},
  month     = {June},
  year      = {2020},
  publisher = {ACM SIGPLAN},
}

REPLica: REPL instrumentation for Coq Analysis

[paper] [github]

Talia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner
CPP 2020
@inproceedings{ringer:2020:replica,
  author = {Ringer, Talia and Sanchez-Stern, Alex and Grossman, Dan and Lerner, Sorin},
  title = {REPLica: REPL Instrumentation for Coq Analysis},
  year = {2020},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/3372885.3373823},
  booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  series = {CPP 2020}
}

Finding Root Causes of Floating Point Error

[paper] [website]

Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, Zachary Tatlock
PLDI 2018
@inproceedings{10.1145/3192366.3192411,
  author = {Sanchez-Stern, Alex and Panchekha, Pavel and Lerner, Sorin and Tatlock, Zachary},
  title = {Finding Root Causes of Floating Point Error},
  year = {2018},
  isbn = {9781450356985},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3192366.3192411},
  doi = {10.1145/3192366.3192411},
  booktitle = {Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation},
  location = {Philadelphia, PA, USA},
  series = {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
@article{fpbench,
  author={Nasrine Damouche and Matthieu Martel and Pavel Panchekha and Jason Qiu and Alex Sanchez-Stern and Zachary Tatlock},
  title={Toward a Standard Benchmark Format and Suite for Floating-Point Analysis},
  series={NSV'16},
  month=July,
  year=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)
@inproceedings{10.1145/2737924.2737959,
  author = {Panchekha, Pavel and Sanchez-Stern, Alex and Wilcox, James R. and Tatlock, Zachary},
  title = {Automatically Improving Accuracy for Floating Point Expressions},
  year = {2015},
  isbn = {9781450334686},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/2737924.2737959},
  doi = {10.1145/2737924.2737959},
  booktitle = {Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation},
  location = {Portland, OR, USA},
  series = {PLDI '15}
}

Contact

You can reach me at alex.sanchezstern@gmail.com. I’m also on GitHub.