Alex Sanchez-Stern

Alex Sanchez-Stern

Hey I’m Alex Sanchez-Stern, I’m a PhD student at the University of California San Diego. I’m also part of the team at the UW that built Herbie. I graduated from the UW with a Masters degree in the Spring of 2016, and started my PhD at UCSD in the Fall of 2016; I’m graduating in the Spring of 2021. I’m generally interested in using programming language techniques to bring hard-fought domain expertise to more everyday programmers. My thesis is on Proverbot9001, a neural-guided proof search tool described on the projects page, and in the MAPL paper below.

Publications

Generating Correctness Proofs with Neural Networks

[paper] [website]

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
@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 alexss@eng.ucsd.edu my university email address. I’m also on GitHub.