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 synthesis to elide complex domain details, and improving the usability of proof assistants through better proof search and new meta-language frameworks. My thesis is on Proverbot9001, a neural-guided proof search tool described below.
Proverbot9001 is a ongoing initiative which uses neural network guided proof search to solve proof obligations in the Coq proof assistant. It has been shown to outperform enumerative and solver-based proof search tools, as well as other state-of-the-art machine-learning based proof search tools. Proverbot9001 is free and open source software, published at MAPL 2020 in June 2020. You can find an extended version of the paper here on my site.
REPLica is a tool that instruments Coq’s interaction model in order to collect fine-grained data on proof developments, as well as a user-study initiative which used the REPLica tool to collect data over the span of a month from a group of intermediate through expert proof engineers. REPLica is free and open source (as well as data), published at CPP 2020 as REPLica: REPL Instrumentation for Coq Analysis.
Herbgrind is a debugging tool to help developers find the root cause of floating-point inaccuracy in large numerical software. It runs directly on program binaries, and produces reports about inaccuracies found that affect program outputs. Herbgrind is free and open source software, published at PLDI 2018 as Finding Root Causes of Floating Point Error.
fpbench is a benchmark format and suite for the development of floating point tooling. I co-authored the original FPBench paper, published at NSV 2016 as Toward a Standard Benchmark Format and Suite for Floating-Point Analysis. Since then, the project has grown to include instutitions and teams across the world.
Herbie is a tool to help scientists and programmers write accurate floating point code more easily. You give it a floating point expression, and it tests it against hundreds of points to find a version that’s more accurate. Herbie is open source software, published at PLDI 2015 as Automatically Improving Accuracy for Floating Point Expressions.