Projects

Lambdelphi learns from human-written proofs to figure out how hard a given proof state is. It’s a collaboration with John Sarracino at Lawrence Livermore National Lab (previously at Cornell).

QEDCartographer uses reinforcement learning to learn how to search for proofs more efficiently. It can produces 26% shorter proofs, in 27% less time. It’s free and open source software that can be found on GitHub.

Passport is a project studying new ways of encoding identifiers for neural models of code in the context of learning-guided foundational verification. It proposes three novel encoding mechanisms for identifiers: a method of indexing common identifiers while storing the category of every identifier (local variable, definition, or constructor), an encoding of the subwords which make up the identifier name, and an encoding of the file and module locations where the identifiers are defined. Passport is free and open source software, and you can find the pre-print paper draft on arXiv.

Proofster is work on interfaces to proof synthesis tools. It exists both in a web version and a plugin for Coq. It was originally published at the ICSE 2023 demo track, you can find the preprint here. Proofster is primarily developed at UIUC by Talia Ringer’s group, headed by Arpan Agrawal.

LFind is a tool for data-driven lemma synthesis. It uses term generalization, synthesis, property-based tasting, and proof-synthesis to try to find useful lemmas for any point in a proof. LFind was published at OOPSLA 2022, you can find the pre-print here. LFind is a collaboration with Todd Millsteins group at UCLA.

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.

Scooter & Sidecar is a new tool for secure database migrations that respect data access policies. The project consists of several languages, for specifying data access policies, specifying migration actions, and maniuplating database values. It also includes tooling for interacting with those languages, automatically enforcing the policies at runtime, running the migrations over existing database, and statically checking that the migrations do not leak data unintentionally. Caravan is work in collaboration with John Renner (UCSD), Fraser Brown (Stanford), and Deian Stefan (UCSD).

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.