I am a part-time lecturer at the University of Washington, where I teach computer science. I specialize in the areas of programming languages and systems.
I also work part-time at Certora, where I work on user education, language design, system architecture, customer acquisition and retention, and business development. My current title is Chief of Technical Market Development. From June 2019 to December 2020, I worked at Certora full time as CTO.
Before joining Certora I was a graduate student at the University of Washington. My research interests are in programming languages and applications of PL techniques to systems, and I continue to be active in research. I'm also a sucker for math, music, and puzzles.
March 29, 2021.
In spring 2021, I am teaching CSEP 505 (Graduate Programming Languages). Check out the course webpage!
January 21, 2021.
Yotam presented our paper at POPL 2021! We show how to combine a little bit of Hamming geometry with deep results from exact learning theory to identify a class of systems and invariants that can be inferred using only a polynomial number of calls to a SAT solver. These results identify a class of relatively easy verification problems, and partially explains why state-of-the-art algorithms perform so well in practice.
December 10, 2020.
I am teaching CSE 374 at UW starting in January. The class teaches the Unix environment, shell scripting, C programming, and a little bit of software engineering. It is intended for students who are not computer science majors. I am excited to experiment with new (to me) ideas about grading and how to foster a communal environment. Check out the course website!
December 10, 2020.
I am transitioning to a part-time role at Certora. I am excited to continue to do the parts of my job there that I really enjoy, and to spend more time on my teaching.
September 30, 2020.
I am teaching UW's undergraduate programming languages course, CSE341, this quarter. Check out the course website!
June 17, 2020.
Jay presented our paper about Armada at PLDI 2020. Armada is a verification system for shared-memory multithreaded programs that allows programmers to write verified systems whose performance matches unverified counterparts, by giving them control over memory layout and choice of synchronization primitives. The key insight is that high-level reasoning principles from the literature can be proved sound against a low-level semantic model that is expressive enough to support these programmer choices. The paper received the distinguished paper award. The talk is also really funny. Check it out!
June 17, 2020.
Chandra presented our paper about Szalinski at PLDI 2020. Szalinski is a tool for decompiling low-level CAD models into higher-level CAD programs that use higher-order functions like map and fold. Szalinski uses E-graphs to efficiently reason about the space of programs that are equivalent to the input model. Chandra gave a great talk. Check it out!
I am a part-time lecturer at the University of Washington. I also work part-time at Certora, as Chief of Technical Market Development.
This is my academic homepage. Before joining Certora I was a graduate student at the University of Washington, where I was advised by Zach Tatlock in the PLSE group. My research interests are in programming languages, systems, and formal methods. My thesis work is on compositional techniques for verifying distributed systems implementations. I generally enjoy working with proof assistants and SMT solvers on applications to all kinds of concurrent programming. I also dabble in floating point, compilers, and 3D printing.
Before grad school, I did my undergraduate at Williams College, graduating in 2013, where I worked with Steve Freund on dynamic race detection. Since then Steve and I have continued to collaborate, including on an "our powers combined" paper on verified dynamic race detection with Cormac Flanagan.
Outside computer science, I enjoy good coffee, choral music, distance running, and small planes. I do not enjoy cars of any size.
I sing baritone in the St. Mark's Cathedral Choir, Evensong Choir, and Compline Choir. The Compline Choir performs each Sunday night at 9:30pm at St. Mark's. The Compline service a 30 minute chanted/sung service that tends to draw hundreds of people every week and thousands via a live radio broadcast and the podcast. It's a classic Seattle experience. You should check it out! You can listen live on King FM or get the podcast.
I occasionally play handbells.
Finally, I like to ride my bike (a Trek 520): in 2009 I biked the TransAm. I'm always thinking about my next tour.
February 21, 2017.
Exercises on Generalizing the Induction Hypothesis.
This post collects several Coq exercises on generalizing the induction hypothesis.
January 9, 2017.
A Port of the Proof of Peterson's Algorithm to Dafny.
This code-only post is a port of the proof of Peterson's Algorithm to Dafny. It also serves as a good example of how to reason about concurrent systems in Dafny, essentially by writing a thread scheduler.
April 24, 2016.
How to build a simple system in Verdi.
In this long-awaited post, we'll show how to implement and verify a simple distributed system using network semantics.
May 8, 2015
A Proof of Peterson's Algorithm.
In this post, we take a break from distributed systems to look at shared memory systems. As a case study, we give a proof that Peterson's algorithm provides mutual exclusion.
April 16, 2015
Network Semantics for Verifying Distributed Systems.
This is the first post in a series on Verdi. In this post, we'll get our feet wet by defining a formal model of how distributed systems execute on the network.
October 20, 2014
Reasoning about Cardinalities of Sums and Products.
In this short, code-heavy post, we extend some of the work from a previous post to reason about the cardinalities of sums and products.
September 14, 2014
Dependent Case Analysis in Coq without Axioms.
This post shows how to get around the limitations of the
destruct tactic when doing case analysis on dependent
types, without resorting to the
dependent destruction tactic,
which relies on additional axioms.
September 4, 2014
"run" + "time" = ???.
This brief post records Mike's description of the three ways of combining the words "run" and "time" in computer science writing.
June 12, 2014
"More Sums than Differences" Sets, Part 2: Counting MSTD Sets.
This is the (much delayed) second post in a series on More Sums than Difference Sets. In this post, we'll take a first crack at the question, "How many MSTD sets are there?" To do so, we'll write a straightforward C program that counts MSTD sets. Then we'll run it to count MSTD sets and benchmark its performance.
April 10, 2014
Tail Recursion Modulo cons.
Tail recursion has come up in a few conversations this week. This post explores a generalization of tail call optimization that I wasn't aware of until Doug described it to me.
March 3, 2014
"More Sums than Differences" Sets, Part 1: A puzzle.
This is the first post in a series on "More Sums than Differences" Sets. In this post, we'll get our terminology straight and ask a lot of questions.
December 31, 2013
Easy access to the off-campus proxy.
I use the UW proxy to access the ACM digital library from off campus, but it's annoying to type the proxy URL every time I click a link to a new paper. Here are two ways to make life easier.