Low-Latency Communication on the IBM RISC System/6000 SP. - Chi-Chao Chang; Grzegorz Czajkowski; Chris Hawblitzel; Thorsten von Eicken (SC, 1996)

The Mobile Object Layer: A Run-Time Substrate for Mobile Adaptive Computations. - Nikos Chrisochoides; Kevin J. Barker; Démian Nave; Chris Hawblitzel (ISCOPE, 1998)

Security versus performance tradeoffs in RPC implementations for safe language systems. - Chi-Chao Chang; Grzegorz Czajkowski; Chris Hawblitzel; Deyu Hu; Thorsten von Eicken (ACM SIGOPS European Workshop, 1998)

Resource management for extensible Internet servers. - Grzegorz Czajkowski; Chi-Chao Chang; Chris Hawblitzel; Deyu Hu; Thorsten von Eicken (ACM SIGOPS European Workshop, 1998)

Implementing Multiple Protection Domains in Java. - Chris Hawblitzel; Chi-Chao Chang; Grzegorz Czajkowski; Deyu Hu; Thorsten von Eicken (USENIX ATC, 1998)

J-Kernel: A Capability-Based Operating System for Java. - Thorsten von Eicken; Chi-Chao Chang; Grzegorz Czajkowski; Chris Hawblitzel; Deyu Hu; Dan Spoonhower (Secure Internet Programming, 1999)

Adding Operating System Structure to Language-Based Protection. - Chris Hawblitzel (2000)

Luna: A Flexible Java Protection System. - Chris Hawblitzel; Thorsten von Eicken (OSDI, 2002)

Deconstructing process isolation. - Mark Aiken; Manuel Fähndrich; Chris Hawblitzel; Galen C. Hunt; James R. Larus (Memory System Performance and Correctness, 2006)

Language support for fast and reliable message-based communication in singularity OS. - Manuel Fähndrich; Mark Aiken; Chris Hawblitzel; Orion Hodson; Galen C. Hunt; James R. Larus; Steven Levi (EuroSys, 2006)

Sealing OS processes to improve dependability and safety. - Galen C. Hunt; Mark Aiken; Manuel Fähndrich; Chris Hawblitzel; Orion Hodson; James R. Larus; Steven Levi; Bjarne Steensgaard; David Tarditi; Ted Wobber (EuroSys, 2007)

Checking the hardware-software interface in spec#. - Kevin Bierhoff; Chris Hawblitzel (PLOS@SOSP, 2007)

A garbage-collecting typed assembly language. - Chris Hawblitzel; Heng Huang; Lea Wittie; Juan Chen (TLDI, 2007)

Type-preserving compilation for large-scale optimizing object-oriented compilers. - Juan Chen; Chris Hawblitzel; Frances Perry; Michael Emmi; Jeremy Condit; Derrick Coetzee; Polyvios Pratikakis (PLDI, 2008)

Helios: heterogeneous multiprocessing with satellite kernels. - Edmund B. Nightingale; Orion Hodson; Ross McIlroy; Chris Hawblitzel; Galen C. Hunt (SOSP, 2009)

Inferable object-oriented typed assembly language. - Ross Tate; Juan Chen; Chris Hawblitzel (PLDI, 2010)

Automated Verification of Practical Garbage Collectors - Chris Hawblitzel; Erez Petrank (Log. Methods Comput. Sci., 2010)

Type safety from the ground up. - Chris Hawblitzel (TLDI, 2011)

Safe to the last instruction: automated verification of a type-safe operating system. - Jean Yang 001; Chris Hawblitzel (Commun. ACM, 2011)

SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs. - Shuvendu K. Lahiri; Chris Hawblitzel; Ming Kawaguchi; Henrique Rebêlo (CAV, 2012)

Towards Modularly Comparing Programs Using Automated Theorem Provers. - Chris Hawblitzel; Ming Kawaguchi; Shuvendu K. Lahiri; Henrique Rebêlo (CADE, 2013)

Will you still compile me tomorrow? static cross-version compiler validation. - Chris Hawblitzel; Shuvendu K. Lahiri; Kshama Pawar; Hammad Hashmi; Sedar Gokbulut; Lakshan Fernando; Dave Detlefs; Scott Wadsworth (ESEC/SIGSOFT FSE, 2013)

Differential assertion checking. - Shuvendu K. Lahiri; Kenneth L. McMillan; Rahul Sharma 001; Chris Hawblitzel (ESEC/SIGSOFT FSE, 2013)

Cosh: Clear OS Data Sharing In An Incoherent World. - Andrew Baumann; Chris Hawblitzel; Kornilios Kourtis; Tim Harris 001; Timothy Roscoe (TRIOS, 2014)

Ironclad Apps: End-to-End Security via Automated Full-System Verification. - Chris Hawblitzel; Jon Howell; Jacob R. Lorch; Arjun Narayan; Bryan Parno; Danfeng Zhang; Brian Zill (OSDI, 2014)

Automated and Modular Refinement Reasoning for Concurrent Programs. - Chris Hawblitzel; Erez Petrank; Shaz Qadeer; Serdar Tasiran (CAV (2), 2015)

Automatic Rootcausing for Program Equivalence Failures in Binaries. - Shuvendu K. Lahiri; Rohit Sinha 001; Chris Hawblitzel (CAV (1), 2015)

IronFleet: proving practical distributed systems correct. - Chris Hawblitzel; Jon Howell; Manos Kapritsos; Jacob R. Lorch; Bryan Parno; Michael Lowell Roberts; Srinath T. V. Setty; Brian Zill (SOSP, 2015)

Everest: Towards a Verified, Drop-in Replacement of HTTPS. - Karthikeyan Bhargavan; Barry Bond; Antoine Delignat-Lavaud; Cédric Fournet; Chris Hawblitzel; Catalin Hritcu; Samin Ishtiaq; Markulf Kohlweiss; K. Rustan M. Leino; Jay R. Lorch; Kenji Maillard; Jianyang Pan; et al. (SNAPL, 2017)

Komodo: Using verification to disentangle secure-enclave hardware from software. - Andrew Ferraiuolo; Andrew Baumann; Chris Hawblitzel; Bryan Parno (SOSP, 2017)

Vale: Verifying High-Performance Cryptographic Assembly Code. - Barry Bond; Chris Hawblitzel; Manos Kapritsos; K. Rustan M. Leino; Jacob R. Lorch; Bryan Parno; Ashay Rane; Srinath T. V. Setty; Laure Thompson (USENIX Security Symposium, 2017)

IronFleet: proving safety and liveness of practical distributed systems. - Chris Hawblitzel; Jon Howell; Manos Kapritsos; Jacob R. Lorch; Bryan Parno; Michael Lowell Roberts; Srinath T. V. Setty; Brian Zill (Commun. ACM, 2017)

Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier. - Guido Martínez; Danel Ahman; Victor Dumitrescu; Nick Giannarakis; Chris Hawblitzel; Catalin Hritcu; Monal Narasimhamurthy; Zoe Paraskevopoulou; Clément Pit-Claudel; Jonathan Protzenko; Tahina Ramananandro; Aseem Rastogi; et al. (CoRR, 2018)

Meta-F ^ star : Proof Automation with SMT, Tactics, and Metaprograms. - Guido Martínez; Danel Ahman; Victor Dumitrescu; Nick Giannarakis; Chris Hawblitzel; Catalin Hritcu; Monal Narasimhamurthy; Zoe Paraskevopoulou; Clément Pit-Claudel; Jonathan Protzenko; Tahina Ramananandro; Aseem Rastogi; et al. (ESOP, 2019)

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. - Jonathan Protzenko; Bryan Parno; Aymeric Fromherz; Chris Hawblitzel; Marina Polubelova; Karthikeyan Bhargavan; Benjamin Beurdouche; Joonwon Choi; Antoine Delignat-Lavaud; Cédric Fournet; Tahina Ramananandro; Aseem Rastogi; et al. (IACR Cryptol. ePrint Arch., 2019)

A verified, efficient embedding of a verifiable assembly language. - Aymeric Fromherz; Nick Giannarakis; Chris Hawblitzel; Bryan Parno; Aseem Rastogi; Nikhil Swamy (Proc. ACM Program. Lang., 2019)

Storage Systems are Distributed Systems (So Verify Them That Way!). - Travis Hance; Andrea Lattuada 001; Chris Hawblitzel; Jon Howell; Rob Johnson 001; Bryan Parno (OSDI, 2020)

EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. - Jonathan Protzenko; Bryan Parno; Aymeric Fromherz; Chris Hawblitzel; Marina Polubelova; Karthikeyan Bhargavan; Benjamin Beurdouche; Joonwon Choi; Antoine Delignat-Lavaud; Cédric Fournet; Natalia Kulatova; Tahina Ramananandro; et al. (SP, 2020)

Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language. - Jay Bosamiya; Sydney Gibson; Yao Li 004; Bryan Parno; Chris Hawblitzel (VSTTE, 2020)

Linear types for large-scale systems verification. - Jialin Li 001; Andrea Lattuada 001; Yi Zhou 025; Jonathan Cameron; Jon Howell; Bryan Parno; Chris Hawblitzel (Proc. ACM Program. Lang., 2022)

Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. - Travis Hance; Yi Zhou 025; Andrea Lattuada 001; Reto Achermann; Alex Conway 001; Ryan Stutsman; Gerd Zellweger; Chris Hawblitzel; Jon Howell; Bryan Parno (OSDI, 2023)

Verus: Verifying Rust Programs using Linear Ghost Types (extended version). - Andrea Lattuada 001; Travis Hance; Chanhee Cho; Matthias Brun 002; Isitha Subasinghe; Yi Zhou 025; Jon Howell; Bryan Parno; Chris Hawblitzel (CoRR, 2023)

Verus: Verifying Rust Programs using Linear Ghost Types. - Andrea Lattuada 001; Travis Hance; Chanhee Cho; Matthias Brun 002; Isitha Subasinghe; Yi Zhou 025; Jon Howell; Bryan Parno; Chris Hawblitzel (Proc. ACM Program. Lang., 2023)

VeriSMo: A Verified Security Module for Confidential VMs. - Ziqiao Zhou; Anjali; Weiteng Chen; Sishuai Gong; Chris Hawblitzel; Weidong Cui (OSDI, 2024)

Verus: A Practical Foundation for Systems Verification. - Andrea Lattuada 001; Travis Hance; Jay Bosamiya; Matthias Brun 002; Chanhee Cho; Hayley LeBlanc; Pranav Srinivasan; Reto Achermann; Tej Chajed; Chris Hawblitzel; Jon Howell; Jacob R. Lorch; et al. (SOSP, 2024)

AutoVerus: Automated Proof Generation for Rust Code. - Chenyuan Yang; Xuheng Li; Md Rakib Hossain Misu; Jianan Yao; Weidong Cui; Yeyun Gong; Chris Hawblitzel; Shuvendu K. Lahiri; Jacob R. Lorch; Shuai Lu; Fan Yang 024; Ziqiao Zhou; et al. (CoRR, 2024)

PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection. - Hayley LeBlanc; Jacob R. Lorch; Chris Hawblitzel; Cheng Huang; Yiheng Tao; Nickolai Zeldovich; Vijay Chidambaram (OSDI, 2025)