Blog
Why buy an expensive desktop computer when your iPhone is a faster SMT solver?
Symbolic Profiling for Scalable Verification and Synthesis
Our OOPSLA’18 paper introduces performance debugging techniques for automated reasoning tools.
Can you train a neural network using an SMT solver?
Yes, and I did, but you shouldn’t.
Building a Program Synthesizer
Build a program synthesis tool, to generate programs from specifications, in 20 lines of code using Rosette.
Memory Consistency Models: A Tutorial
The cause of, and solution to, all your multicore performance problems.
SNAPL rejected my crazy abstract, so I’m sharing my craziness with the world instead.
An introduction to the field of program synthesis, the idea that computers can write programs automatically if we just tell them what we want.
How Not to Measure Computer System Performance
In a recent Sampa group meeting, I spoke about the many pitfalls in measuring computer system performance.
News
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!
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.
On the AWS Storage blog, we wrote a post about how we’re using formal methods to build Amazon S3.
Our paper on Diospyros, a new synthesis-aided compiler for DSPs, will appear at ASPLOS 2021.
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.
The SIGPLAN blog published an article I wrote about the state of program synthesis in 2019.
I defended my PhD!
The video from my OOPSLA 2018 talk on profiling symbolic evaluation engines is now available.
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.
I was interviewed for the People of Programming Languages series at POPL 2018.
The video from my PLDI 2017 talk about memory model synthesis is available.
Our paper Synthesizing Memory Models from Framework Sketches and Litmus Tests will appear at PLDI 2017! More info on the MemSynth homepage.
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!
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.
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!
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.
Our work on using DNA for digital data storage is featured in the New York Times.
Our paper on optimal program synthesis, Optimizing Synthesis with Metasketches, will appear at POPL 2016!
I’m on the artifact evaluation committee for POPL’16.
Read about Uncertain<T> in IEEE Micro as part of their Top Picks from the Computer Architecture Conferences special issue.
Adrian, Luis and I have a paper on hardware–software co-design at SNAPL.
Uncertain<T> was selected to appear in IEEE Micro’s Top Picks from the Computer Architecture Conferences special issue later this year!
I’ll be on the artifact evaluation committee for PLDI’15.
Our Uncertain<T> paper was selected as a SIGPLAN Research Highlight. How cool is that!