I’m an assistant professor in the Department of Computer Science at the University of Texas at Austin.
I work in programming languages, formal methods, and systems. My research helps programmers build more reliable software using automated programming tools: verification tools that check program correctness, and synthesis tools that generate correct programs from specifications. I work to make automated programming tools easier to build and use, and deploy them at scale on applications in systems and architecture.
I’m also a visiting researcher at Amazon Web Services, where I work on automated reasoning for Amazon S3.
I received my PhD in 2019 from the University of Washington, where I was advised by Emina Torlak, Dan Grossman, and Luis Ceze. I also have a bachelors from the Australian National University.
News
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.
Teaching
- CS 395T: Systems Verification and Synthesis: Spring 2023, Spring 2022, Spring 2021
- CS 345H/386L: Programming Languages: Fall 2022
Students
- Nathan Taylor
- Sammy Thomas
- Dani Wang
- Alumni
- Stefan deBruyn
- Owen Graves
Publications
[DBLP]
Conference Papers
Chipmunk: Investigating Crash-Consistency in Persistent-Memory File Systems.
Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors.
Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3.
SOSP 2021. Best Paper Award.
Vectorization for Digital Signal Processors via Equality Saturation.
Automatic Generation of High-Performance Quantized Machine Learning Kernels.
Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval.
SOSP 2019. Best Paper Award. Distinguished Artifact Award.
Finding Code That Explodes Under Symbolic Evaluation.
OOPSLA 2018. Distinguished Artifact Award.
Nickel: A Framework for Design and Verification of Information Flow Control Systems.
Synthesizing Memory Models from Framework Sketches and Litmus Tests.
Push-Button Verification of File Systems via Crash Refinement.
OSDI 2016. Best Paper Award.
Specifying and Checking File System Crash-Consistency Models.
A DNA-Based Archival Storage System.
ASPLOS 2016. IEEE Micro Top Picks.
Uncertain<T>: A First-Order Type for Uncertain Data.
ASPLOS 2014. SIGPLAN Research Highlight. IEEE Micro Top Picks.
Journal Papers
Noninterference Specifications for Secure Systems.
ACM SIGOPS Operating Systems Review, vol. 54, no. 1, pp. 31–39, July 2020.
A Taxonomy of General Purpose Approximate Computing Techniques.
IEEE Embedded Systems Letters, vol. 10, no. 1, pp. 2–5, March 2018.
Toward a DNA-Based Archival Storage System.
IEEE Micro, vol. 37, no. 3, pp. 98–104, May–June 2017.
Uncertain<T>: Abstractions for Uncertain Hardware and Software.
IEEE Micro, vol. 35, no. 3, pp. 132–143, May–June 2015.
Workshop Papers
Scaling Program Synthesis by Exploiting Existing Code.
ML4PL 2015 (colocated with ECOOP 2015).
REACT: A Framework for Rapid Exploration of Approximate Computing Techniques.
There's Something About Bayes: Effective Probabilistic Programming for the Rest of Us.
APPROX 2014 (colocated with PLDI 2014).
Posters & Talks
Uncertain<T>: A First-Order Type for Uncertain Data.
PLDI 2013 Student Research Competition. First Place, PLDI Student Research Competition. Second Place, ACM Student Research Competition Grand Final.
The Model Is Not Enough: Understanding Energy Consumption in Mobile Devices.
Theses
Optimizing the Automated Programming Stack.
PhD thesis, University of Washington, 2019.
Abstractions and Techniques for Programming with Uncertain Data.
Honours thesis, Bachelor of Philosophy (Honours), Australian National University, 2013.