James Bornholt

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 the Amazon S3 object storage service.

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
[Subscribe]

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.

Older News...

Teaching

CS 395T: Systems Verification and Synthesis: Spring 2023, Spring 2022, Spring 2021
CS 345H/386L: Programming Languages: Spring 2024, Fall 2022

Students

Nathan Taylor PhD, 2021–
Sammy Thomas PhD, 2021–
Dani Wang PhD, 2021–

Publications
[DBLP]

[Google Scholar]

Conference Papers

Automatic Generation of Vectorizing Compilers for Customizable Digital Signal Processors.

Samuel Thomas and James Bornholt.

ASPLOS 2024.
- Paper (PDF)
Synthesis-Aided Crash Consistency for Storage Systems.

Jacob Van Geffen, Xi Wang, Emina Torlak, and James Bornholt.

ECOOP 2023.
- Paper (PDF)
Chipmunk: Investigating Crash-Consistency in Persistent-Memory File Systems.

Hayley LeBlanc, Shankara Pailoor, Om Saran, Isil Dillig, James Bornholt, and Vijay Chidambaram.

EuroSys 2023. Best Paper Award.
- Paper (PDF)
- Code
Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors.

Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, and Isil Dillig.

OOPSLA 2022.
- Paper (PDF)
- Code
Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3.

James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, and Andrew Warfield.

SOSP 2021. Best Paper Award.
- Paper (PDF)
- Slides
- Video
- Poster
Vectorization for Digital Signal Processors via Equality Saturation.

Alexa VanHattum, Rachit Nigam, Vincent T. Lee, James Bornholt, and Adrian Sampson.

ASPLOS 2021.
- Paper (PDF)
- Code
A Synthesis-Aided Compiler for DSP Architectures.

Alexa VanHattum, Rachit Nigam, Vincent T. Lee, James Bornholt, and Adrian Sampson.

LCTES 2020.
- Paper (PDF)
- Code
Automatic Generation of High-Performance Quantized Machine Learning Kernels.

Meghan Cowan, Thierry Moreau, Tianqi Chen, James Bornholt, and Luis Ceze.

CGO 2020.
- Paper (PDF)
- Artifact
Fixing Code That Explodes Under Symbolic Evaluation.

Sorawee Porncharoenwase, James Bornholt, and Emina Torlak.

VMCAI 2020.
- Paper (PDF)
- Project Homepage
- Code
Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval.

Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang.

SOSP 2019. Best Paper Award. Distinguished Artifact Award.
- Paper (PDF)
- Project Homepage
- Artifact
Finding Code That Explodes Under Symbolic Evaluation.

James Bornholt and Emina Torlak.

OOPSLA 2018. Distinguished Artifact Award.
- Paper (PDF)
- Slides
- Video
- Project Homepage
- Artifact
- Documentation
Nickel: A Framework for Design and Verification of Information Flow Control Systems.

Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang.

OSDI 2018.
- Paper (PDF)
- Slides
- Project Homepage
Hyperkernel: Push-Button Verification of an OS Kernel.

Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang.

SOSP 2017.
- Paper (PDF)
- Slides
- Project Homepage
Synthesizing Memory Models from Framework Sketches and Litmus Tests.

James Bornholt and Emina Torlak.

PLDI 2017.
- Paper (PDF)
- Slides
- Video
- Project Homepage
- Artifact
- Source Code
Push-Button Verification of File Systems via Crash Refinement.

Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang.

OSDI 2016. Best Paper Award.
- Paper (PDF)
- Slides
- Project Homepage
Disciplined Inconsistency with Consistency Types.

Brandon Holt, James Bornholt, Irene Zhang, Dan R. K. Ports, Mark Oskin, and Luis Ceze.

SoCC 2016.
- Paper (PDF)
Specifying and Checking File System Crash-Consistency Models.

James Bornholt, Antoine Kaufmann, Jialin Li, Arvind Krishnamurthy, Emina Torlak, and Xi Wang.

ASPLOS 2016.
- Paper (PDF)
- Slides
- Project Homepage
- Source Code
A DNA-Based Archival Storage System.

James Bornholt, Randolph Lopez, Douglas M. Carmean, Luis Ceze, Georg Seelig, and Karin Strauss.

ASPLOS 2016. IEEE Micro Top Picks.
- Paper (PDF)
- Slides
Optimizing Synthesis with Metasketches.

James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze.

POPL 2016.
- Paper (PDF)
- Slides
- Video
- Project Homepage
- Artifact
- Source Code
Hardware–Software Co-Design: Not Just a Cliché.

Adrian Sampson, James Bornholt, and Luis Ceze.

SNAPL 2015.
- Paper (PDF)
Uncertain<T>: A First-Order Type for Uncertain Data.

James Bornholt, Todd Mytkowicz, and Kathryn S. McKinley.

ASPLOS 2014. SIGPLAN Research Highlight. IEEE Micro Top Picks.
- Paper (PDF)
- Slides
- Poster

Journal Papers

Noninterference Specifications for Secure Systems.

Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, and Xi Wang.

ACM SIGOPS Operating Systems Review, vol. 54, no. 1, pp. 31–39, July 2020.
- Paper (PDF)
A Taxonomy of General Purpose Approximate Computing Techniques.

Thierry Moreau, Joshua San Miguel, Mark Wyse, James Bornholt, Armin Alaghi, Luis Ceze, Natalie Enright Jerger, and Adrian Sampson.

IEEE Embedded Systems Letters, vol. 10, no. 1, pp. 2–5, March 2018.
- Paper (PDF)
Toward a DNA-Based Archival Storage System.

James Bornholt, Randolph Lopez, Douglas M. Carmean, Luis Ceze, Georg Seelig, and Karin Strauss.

IEEE Micro, vol. 37, no. 3, pp. 98–104, May–June 2017.
- Paper (PDF)
Uncertain<T>: Abstractions for Uncertain Hardware and Software.

James Bornholt, Todd Mytkowicz, and Kathryn S. McKinley.

IEEE Micro, vol. 35, no. 3, pp. 132–143, May–June 2015.
- Paper (PDF)

Workshop Papers

Scaling Program Synthesis by Exploiting Existing Code.

James Bornholt and Emina Torlak.

ML4PL 2015 (colocated with ECOOP 2015).
- Paper (PDF)
- Slides
Approximate Program Synthesis.

James Bornholt, Emina Torlak, Luis Ceze, and Dan Grossman.

WAX 2015 (colocated with PLDI 2015).
- Paper (PDF)
- Slides
REACT: A Framework for Rapid Exploration of Approximate Computing Techniques.

Mark Wyse, Andre Baixo, Thierry Moreau, Bill Zorn, James Bornholt, Adrian Sampson, Luis Ceze, and Mark Oskin.

WAX 2015 (colocated with PLDI 2015).
- Paper (PDF)
- Slides
Programming the Internet of Uncertain <T>hings.

James Bornholt, Na Meng, Todd Mytkowicz, and Kathryn S. McKinley.

SCAW 2015 (colocated with HPCA 2015).
- Paper (PDF)
- Slides
There's Something About Bayes: Effective Probabilistic Programming for the Rest of Us.

James Bornholt, Todd Mytkowicz, and Kathryn S. McKinley.

APPROX 2014 (colocated with PLDI 2014).
- Paper (PDF)
- Slides

Posters & Talks

Uncertain<T>: A First-Order Type for Uncertain Data.

James Bornholt.

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.

James Bornholt, Todd Mytkowicz, and Kathryn S. McKinley.

Hot Chips 24, 2012.
- Extended Abstract
- Poster

Theses

Optimizing the Automated Programming Stack.

James Bornholt.

PhD thesis, University of Washington, 2019.
- Thesis
- Slides
Abstractions and Techniques for Programming with Uncertain Data.

James Bornholt.

Honours thesis, Bachelor of Philosophy (Honours), Australian National University, 2013.
- Thesis
- Slides

News [Subscribe]