James Bornholt

Employment

• Amazon Web Services

  Austin, TX, USA

  Principal Applied Scientist, Amazon S3

  2022–

  Senior Applied Scientist, Amazon S3

  2019–2022

  Research Intern, Automated Reasoning Group

  2018

• University of Texas at Austin

  Austin, TX, USA

  Assistant Professor, Department of Computer Science

  2021–2024

• Microsoft Research

  Seattle, WA, USA

  Software Engineer, Research in Software Engineering (RiSE) group

  2014

  Research Intern, Research in Software Engineering (RiSE) group

  2012–2013

  Research Intern, Research in Software Engineering (RiSE) group

  2011–2012

Education

• University of Washington

  Seattle, WA, USA

  Ph.D., Computer Science & Engineering

  2014–2019

  • Advisors: Emina Torlak, Dan Grossman, Luis Ceze

  • Thesis: Optimizing the Automated Programming Stack

  M.S., Computer Science & Engineering

  2016

• Australian National University

  Canberra, Australia

  Bachelor of Philosophy (Honours)

  2010–2013

  • Advisor: Steve Blackburn

  • First Class Honours and the University Medal in Computer Science

Publications

Conference Papers

• SquirrelFS: using the Rust compiler to check file-system crash consistency. Hayley LeBlanc, Nathan Taylor, James Bornholt and Vijay Chidambaram. OSDI 2024.

• Automatic Generation of Vectorizing Compilers for Customizable Digital Signal Processors. Samuel Thomas and James Bornholt. ASPLOS 2024. Best Paper Award.

• Synthesis-Aided Crash Consistency for Storage Systems. Jacob Van Geffen, Xi Wang, Emina Torlak, and James Bornholt. ECOOP 2023.

• 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.

• Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors. Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, and Isil Dillig. OOPSLA 2022.

• 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.

• Vectorization for Digital Signal Processors via Equality Saturation. Alexa VanHattum, Rachit Nigam, Vincent T. Lee, James Bornholt, and Adrian Sampson. ASPLOS 2021.

• A Synthesis-Aided Compiler for DSP Architectures. Alexa VanHattum, Rachit Nigam, Vincent T. Lee, James Bornholt, and Adrian Sampson. LCTES 2020.

• Automatic Generation of High-Performance Quantized Machine Learning Kernels. Meghan Cowan, Thierry Moreau, Tianqi Chen, James Bornholt, and Luis Ceze. CGO 2020.

• Fixing Code That Explodes Under Symbolic Evaluation. Sorawee Porncharoenwase, James Bornholt, and Emina Torlak. VMCAI 2020.

• 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.

• Finding Code That Explodes Under Symbolic Evaluation. James Bornholt and Emina Torlak. OOPSLA 2018. Distinguished Artifact Award.

• 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.

• 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.

• Synthesizing Memory Models from Framework Sketches and Litmus Tests. James Bornholt and Emina Torlak. PLDI 2017.

• Push-Button Verification of File Systems via Crash Refinement. Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. OSDI 2016. Best Paper Award.

• Disciplined Inconsistency with Consistency Types. Brandon Holt, James Bornholt, Irene Zhang, Dan R. K. Ports, Mark Oskin, and Luis Ceze. SoCC 2016.

• Specifying and Checking File System Crash-Consistency Models. James Bornholt, Antoine Kaufmann, Jialin Li, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. ASPLOS 2016.

• 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.

• Optimizing Synthesis with Metasketches. James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. POPL 2016.

• Hardware–Software Co-Design: Not Just a Cliché. Adrian Sampson, James Bornholt, and Luis Ceze. SNAPL 2015.

• 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.

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.

• 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.

• 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.

• 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.

Workshop Papers

• Scaling Program Synthesis by Exploiting Existing Code. James Bornholt and Emina Torlak. ML4PL 2015 (colocated with ECOOP 2015).

• Approximate Program Synthesis. James Bornholt, Emina Torlak, Luis Ceze, and Dan Grossman. WAX 2015 (colocated with PLDI 2015).

• 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).

• Programming the Internet of Uncertain <T>hings. James Bornholt, Na Meng, Todd Mytkowicz, and Kathryn S. McKinley. SCAW 2015 (colocated with HPCA 2015).

• 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).

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.

Theses

• Optimizing the Automated Programming Stack. James Bornholt. PhD thesis, University of Washington, 2019.

• Abstractions and Techniques for Programming with Uncertain Data. James Bornholt. Honours thesis, Bachelor of Philosophy (Honours), Australian National University, 2013.

Awards

• ASPLOS Best Paper Award

  2024

• EuroSys Best Paper Award

  2023

• SOSP Best Paper Award

  2021

• SOSP Best Paper Award

  2019

• OOPSLA Distinguished Artifact Award

  2018

• Facebook Ph.D. Fellowship

  2018–2020

• IEEE Micro Top Picks from the Computer Architecture Conferences, for DNA storage

  2017

• OSDI Jay Lepreau Best Paper Award

  2016

• IEEE Micro Top Picks from the Computer Architecture Conferences, for Uncertain<T>

  2015

• ACM SIGPLAN Research Highlight, for Uncertain<T>

  2014

• David Notkin Endowed Graduate Fellowship, University of Washington

  2014–2015

• Second Place, ACM Student Research Competition Grand Finals (undergraduate)

  2014

• First Place, ACM PLDI Student Research Competition (undergraduate)

  2013

• ANU University Medal for Computer Science

  2013

Teaching

• CS 395T: Systems Verification and Synthesis

  University of Texas at Austin

  Instructor

  Spring 2023

  Instructor

  Spring 2022

  Instructor

  Spring 2021

• CS 345H/386L: Programming Languages

  University of Texas at Austin

  Instructor

  Spring 2024

  Instructor

  Fall 2022

• CSE 507, Computer Aided Reasoning for Software

  University of Washington

  Teaching Assistant

  Winter 2017

  Teaching Assistant

  Spring 2016

Students

• Nathan Taylor (PhD)

  2021–

• Sammy Thomas (PhD)

  2021–

• Dani Wang (PhD)

  2021–

• Julia Benginow (BS Honors)

  2023–2024

• Finn Frankis (BS Honors)

  2022–2023

• Stefan Debruyn (BS Honors)

  2021–2022

• Owen Graves (BS Honors)

  2020–2021

Service

Program Committees

• Symposium on Operating Systems Principles (SOSP) — Program Committee

  2024

• Programming Languages Design and Implementation (PLDI) — Program Committee

  2024

• European Conference on Computer Systems (EuroSys) — Program Committee

  2024

• Architectural Support for Programming Languages and Operating Systems (ASPLOS) — External Review Committee

  2024

• Architectural Support for Programming Languages and Operating Systems (ASPLOS) — Program Committee

  2023

• Programming Languages Design and Implementation (PLDI) — Program Committee

  2022

• Architectural Support for Programming Languages and Operating Systems (ASPLOS) — External Review Committee

  2022

• Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) — External Review Committee

  2021

• Operating Systems Design and Implementation (OSDI) — Program Committee

  2021

• Architectural Support for Programming Languages and Operating Systems (ASPLOS) — Program Committee

  2021

• Programming Languages Design and Implementation (PLDI) — Program Committee

  2020

• Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) — Review Committee

  2020

• Architectural Support for Programming Languages and Operating Systems (ASPLOS) — External Review Committee

  2020

• Principles and Practice of Parallel Programming (PPoPP) — Brief Announcements Program Committee

  2020

• Formal Techniques for Java-Like Programs (FTfJP) — Program Committee

  2019

• Programming Languages Design and Implementation (PLDI) — External Review Committee

  2017

• Computer-Aided Verification (CAV) — Artifact Evaluation Committee

  2017

• Principles of Programming Languages (POPL) — Artifact Evaluation Committee

  2016

• Programming Languages Design and Implementation (PLDI) — Artifact Evaluation Committee

  2015

Reviewing

• Symposium on Operating Systems Principles (SOSP)

  2023

• National Science Foundation (NSF) panel member

  2022

• National Science Foundation (NSF) panel member

  2021

• Architectural Support for Programming Languages and Operating Systems (ASPLOS)

  2018

• IEEE Transactions on Emerging Topics in Computing

  2017

• Computer-Aided Verification (CAV)

  2015

• ACM Transactions on Embedded Computing

  2015

• Architectural Support for Programming Languages and Operating Systems (ASPLOS)

  2015

Department Service

• Undergrduate Curriculum Committee, Computer Science, University of Texas at Austin

  2022

• PhD Admissions Committee, Computer Science, University of Texas at Austin

  2021, 2022

• Graduate Admissions Committee, Computer Science & Engineering, University of Washington

  2017, 2018, 2019

• Prospective Student Committee Co-Chair, Computer Science & Engineering, University of Washington

  2016

• Prospective Student Committee, Computer Science & Engineering, University of Washington

  2015–2019

Student Committees

• Sekwon Lee, PhD Dissertation Committee

  2023

• Soujanya Ponnapalli, PhD Dissertation Committee

  2023

• Aashaka Shah, PhD Dissertation Committee

  2023

• Rohan Kadekodi, PhD Dissertation Committee

  2023

• Henrique Fingler, PhD Dissertation Committee

  2023

• Mihir Mehta, PhD Dissertation Committee

  2021

• Kostas Ferlas, PhD Dissertation Committee

  2020

Presentations and Seminars

• Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3

  • High Confidence Software and Systems conference, Invited Talk

    May 2022

  • Facebook, Invited Talk

    Apr 2022

  • SOSP, Conference Talk

    Oct 2021

  • New England Systems Verification Day, Invited Talk

    Oct 2021

• Program Synthesis in the Small

  • Purdue University, Invited Talk

    Oct 2020

• Synthesizing System Specifications

  • State of the Art in Program Synthesis, Invited Talk

    Sep 2019

• Optimizing the Automated Programming Stack

  • Australian National University, Invited Talk

    Jul 2019

  • University of Toronto, Invited Seminar

    Apr 2019

  • Princeton University, Invited Seminar

    Apr 2019

  • University of British Columbia, Invited Seminar

    Apr 2019

  • École Polytechnique Fédérale de Lausanne, Invited Seminar

    Apr 2019

  • University of Massachusetts Amherst, Invited Seminar

    Apr 2019

  • Northeastern University, Invited Seminar

    Mar 2019

  • Microsoft Research, Invited Seminar

    Mar 2019

  • Georgia Institute of Technology, Invited Seminar

    Mar 2019

  • University of California, Berkeley, Invited Seminar

    Feb 2019

  • Brown University, Invited Seminar

    Feb 2019

  • Carnegie Mellon University, Invited Seminar

    Feb 2019

  • University of Maryland, College Park, Invited Seminar

    Feb 2019

  • University of Texas at Austin, Invited Seminar

    Feb 2019

  • Cornell University, Invited Seminar

    Jan 2019

• Finding Code That Explodes Under Symbolic Evaluation

  • University of California, Santa Cruz, Guest Lecture

    Nov 2019

  • OOPSLA, Conference Talk

    Nov 2018

  • Galois, Invited Talk

    Jun 2018

• Ocelot: Relational Logic in a Solver-Aided Language

  • Future of Alloy Workshop, Invited Talk

    Apr 2018

• Synthesizing Memory Models from Framework Sketches and Litmus Tests

  • PLDI, Conference Talk

    Jun 2017

• Programming with Estimates

  • Programming Languages Mentoring Workshop, Invited Talk

    Jun 2016

• Specifying and Checking File-System Crash Consistency Models

  • DARPA BRASS PI Meeting, Invited Talk

    Jul 2016

  • ASPLOS, Conference Talk

    Apr 2016

• A DNA-Based Archival Storage System

  • ASPLOS, Conference Talk

    Apr 2016

• Optimizing Synthesis with Metasketches

  • POPL, Conference Talk

    Jan 2016

  • Dagstuhl Seminar 15491 (Approximate and Probabilistic Computing), Invited Talk

    Dec 2015

Funding

• NSF Formal Methods in the Field (FMiTF), $375k

  2021–2025

• Google Research Scholar, $60k

  2022

• Amazon, $70k

  2021