5 November 2018

SMT Solving on an iPhone

Why buy an expensive desktop computer when your iPhone is a faster SMT solver?

17 October 2018

Symbolic Profiling for Scalable Verification and Synthesis

Our OOPSLA’18 paper introduces performance debugging techniques for automated reasoning tools.

2 August 2018

Can you train a neural network using an SMT solver?

Yes, and I did, but you shouldn’t.

10 July 2018

Building a Program Synthesizer

Build a program synthesis tool, to generate programs from specifications, in 20 lines of code using Rosette.

17 February 2016

Memory Consistency Models: A Tutorial

The cause of, and solution to, all your multicore performance problems.

23 February 2015

Monte Carlo Benchmarking

SNAPL rejected my crazy abstract, so I’m sharing my craziness with the world instead.

6 January 2015

Program Synthesis Explained

An introduction to the field of program synthesis, the idea that computers can write programs automatically if we just tell them what we want.

17 November 2014

How Not to Measure Computer System Performance

In a recent Sampa group meeting, I spoke about the many pitfalls in measuring computer system performance.


15 September 2023

Two fun new papers! Our work on synthesized soft updates for crash consistency appeared at ECOOP 2023. Sammy’s work on Isaria, a framework for automatically building vectorizing compilers for weird architectures, will appear at ASPLOS 2024!

14 March 2023

From the AWS side of my head on Pi Day: our thoughts on building a reliable and fast user-space file system for Amazon S3.

22 October 2021

On the AWS Storage blog, we wrote a post about how we’re using formal methods to build Amazon S3.

29 September 2021

We have a new paper at SOSP 2021 about applying lightweight formal methods to validate ShardStore, Amazon S3’s new storage node software. As part of this work, we open-sourced a new stateless model checker for Rust called Shuttle, which is great at finding subtle concurrency bugs.

21 November 2020

Our paper on Diospyros, a new synthesis-aided compiler for DSPs, will appear at ASPLOS 2021.

7 November 2019

Our SOSP paper on scaling automated verification won best paper and distinguished artifact awards! We also have two new papers: at VMCAI 2020 on automatically fixing performance issues in solver-aided tools, and at CGO 2020 on synthesizing high-performance quantized machine learning kernels.

31 July 2019

The SIGPLAN blog published an article I wrote about the state of program synthesis in 2019.

29 May 2019

I defended my PhD!

21 November 2018
24 August 2018

Our paper on profiling symbolic evaluation engines will appear at OOPSLA 2018! The new symbolic profiler is integrated into Rosette, so you can try it out right now.

18 December 2017

I was interviewed for the People of Programming Languages series at POPL 2018.

27 June 2017

The video from my PLDI 2017 talk about memory model synthesis is available.

13 April 2017
30 January 2017

Our work on DNA storage was selected to appear in IEEE Micro’s Top Picks from the Computer Architecture Conferences special issue later this year!

12 July 2016

I was lucky enough to speak at the Programming Languages Mentoring Workshop at PLDI this year about our work on Uncertain<T>. You can watch the talk (sorry about the quality!) or check out the slides.

18 June 2016

Back in January, I presented our paper on Optimizing Synthesis with Metasketches at POPL 2016. If you weren’t there, you can now watch the talk on YouTube!

12 April 2016

I presented our two papers, on file system crash-consistency models and DNA storage, at ASPLOS 2016. The internet is awash with cat pictures thanks to coverage of our DNA storage work; see the Daily Mail, The Register, or Gizmodo.

3 December 2015

Our work on using DNA for digital data storage is featured in the New York Times.

5 October 2015

Our paper on optimal program synthesis, Optimizing Synthesis with Metasketches, will appear at POPL 2016!

6 August 2015
22 June 2015
14 April 2015
15 February 2015

Uncertain<T> was selected to appear in IEEE Micro’s Top Picks from the Computer Architecture Conferences special issue later this year!

16 January 2015
10 November 2014

Our Uncertain<T> paper was selected as a SIGPLAN Research Highlight. How cool is that!