Chris Hawblitzel

53 papers A* 17A 5B 1Journal 13Unranked 16
YearRankTypeTitle / Venue / Authors
2025 J jnl
AutoVerus: Automated Proof Generation for Rust Code.
Proc. ACM Program. Lang.
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, Ziqiao Zhou, Shan Lu
2025 A* conf
PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection.
OSDI
Hayley LeBlanc, Jacob R. Lorch, Chris Hawblitzel, Cheng Huang, Yiheng Tao, Nickolai Zeldovich, Vijay Chidambaram
2025 J jnl
Tunable Automation in Automated Program Verification.
CoRR
Alexander Y. Bai, Chris Hawblitzel, Andrea Lattuada
2025 J jnl
VeruSAGE: A Study of Agent-Based Verification for Rust Systems.
CoRR
Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jacob R. Lorch, Shan Lu
2024 J jnl
AutoVerus: Automated Proof Generation for Rust Code.
CoRR
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, Ziqiao Zhou, Shan Lu
2024 A* conf
VeriSMo: A Verified Security Module for Confidential VMs.
OSDI
Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, Weidong Cui
2024 A* conf
Verus: A Practical Foundation for Systems Verification.
SOSP
Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon, Bryan Parno
2023 A* conf
Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems.
OSDI
Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, Bryan Parno
2023 J jnl
Verus: Verifying Rust Programs using Linear Ghost Types (extended version).
CoRR
Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel
2023 J jnl
Verus: Verifying Rust Programs using Linear Ghost Types.
Proc. ACM Program. Lang.
Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel
2022 J jnl
Linear types for large-scale systems verification.
Proc. ACM Program. Lang.
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, Chris Hawblitzel
2020 A* conf
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
SP
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, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
2020 A* conf
Storage Systems are Distributed Systems (So Verify Them That Way!).
OSDI
Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, Bryan Parno
2020 — conf
Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language.
VSTTE
Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel
2019 J jnl
A verified, efficient embedding of a verifiable assembly language.
Proc. ACM Program. Lang.
Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, Nikhil Swamy
2019 J jnl
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
IACR Cryptol. ePrint Arch.
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, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
2019 A conf
Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms.
ESOP
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, Nikhil Swamy
2018 J jnl
Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier.
CoRR
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, Nikhil Swamy
2017 — conf
Everest: Towards a Verified, Drop-in Replacement of HTTPS.
SNAPL
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, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean Karim Zinzindohoue
2017 J jnl
IronFleet: proving safety and liveness of practical distributed systems.
Commun. ACM
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael Lowell Roberts, Srinath T. V. Setty, Brian Zill
2017 A* conf
Komodo: Using verification to disentangle secure-enclave hardware from software.
SOSP
Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, Bryan Parno
2017 A* conf
Vale: Verifying High-Performance Cryptographic Assembly Code.
USENIX Security Symposium
Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath T. V. Setty, Laure Thompson
2015 — conf
Automated and Modular Refinement Reasoning for Concurrent Programs.
CAV (2)
Chris Hawblitzel, Erez Petrank, Shaz Qadeer, Serdar Tasiran
2015 — conf
Automatic Rootcausing for Program Equivalence Failures in Binaries.
CAV (1)
Shuvendu K. Lahiri, Rohit Sinha, Chris Hawblitzel
2015 A* conf
IronFleet: proving practical distributed systems correct.
SOSP
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael Lowell Roberts, Srinath T. V. Setty, Brian Zill
2014 — conf
Cosh: Clear OS Data Sharing In An Incoherent World.
TRIOS
Andrew Baumann, Chris Hawblitzel, Kornilios Kourtis, Tim Harris, Timothy Roscoe
2014 A* conf
Ironclad Apps: End-to-End Security via Automated Full-System Verification.
OSDI
Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, Brian Zill
2013 — conf
Differential assertion checking.
ESEC/SIGSOFT FSE
Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, Chris Hawblitzel
2013 A conf
Towards Modularly Comparing Programs Using Automated Theorem Provers.
CADE
Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, Henrique Rebêlo
2013 — conf
Will you still compile me tomorrow? static cross-version compiler validation.
ESEC/SIGSOFT FSE
Chris Hawblitzel, Shuvendu K. Lahiri, Kshama Pawar, Hammad Hashmi, Sedar Gokbulut, Lakshan Fernando, Dave Detlefs, Scott Wadsworth
2012 B ed.
Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings
CPP
Chris Hawblitzel, Dale Miller
2012 A* conf
SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs.
CAV
Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Rebêlo
2011 J jnl
Safe to the last instruction: automated verification of a type-safe operating system.
Commun. ACM
Jean Yang, Chris Hawblitzel
2011 — conf
Type safety from the ground up.
TLDI
Chris Hawblitzel
2010 J jnl
Automated Verification of Practical Garbage Collectors
Log. Methods Comput. Sci.
Chris Hawblitzel, Erez Petrank
2010 A* conf
Inferable object-oriented typed assembly language.
PLDI
Ross Tate, Juan Chen, Chris Hawblitzel
2010 A* conf
Safe to the last instruction: automated verification of a type-safe operating system.
PLDI
Jean Yang, Chris Hawblitzel
2009 A* conf
Automated verification of practical garbage collectors.
POPL
Chris Hawblitzel, Erez Petrank
2009 A* conf
Helios: heterogeneous multiprocessing with satellite kernels.
SOSP
Edmund B. Nightingale, Orion Hodson, Ross McIlroy, Chris Hawblitzel, Galen C. Hunt
2008 A* conf
Type-preserving compilation for large-scale optimizing object-oriented compilers.
PLDI
Juan Chen, Chris Hawblitzel, Frances Perry, Michael Emmi, Jeremy Condit, Derrick Coetzee, Polyvios Pratikakis
2007 — conf
A garbage-collecting typed assembly language.
TLDI
Chris Hawblitzel, Heng Huang, Lea Wittie, Juan Chen
2007 — conf
Checking the hardware-software interface in spec#.
PLOS@SOSP
Kevin Bierhoff, Chris Hawblitzel
2007 A conf
Sealing OS processes to improve dependability and safety.
EuroSys
Galen C. Hunt, Mark Aiken, Manuel Fähndrich, Chris Hawblitzel, Orion Hodson, James R. Larus, Steven Levi, Bjarne Steensgaard, David Tarditi, Ted Wobber
2006 — conf
Deconstructing process isolation.
Memory System Performance and Correctness
Mark Aiken, Manuel Fähndrich, Chris Hawblitzel, Galen C. Hunt, James R. Larus
2006 A conf
Language support for fast and reliable message-based communication in singularity OS.
EuroSys
Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen C. Hunt, James R. Larus, Steven Levi
2002 A* conf
Luna: A Flexible Java Protection System.
OSDI
Chris Hawblitzel, Thorsten von Eicken
2000 — —
Adding Operating System Structure to Language-Based Protection.
Chris Hawblitzel
1999 — conf
J-Kernel: A Capability-Based Operating System for Java.
Secure Internet Programming
Thorsten von Eicken, Chi-Chao Chang, Grzegorz Czajkowski, Chris Hawblitzel, Deyu Hu, Dan Spoonhower
1998 — conf
Implementing Multiple Protection Domains in Java.
USENIX ATC
Chris Hawblitzel, Chi-Chao Chang, Grzegorz Czajkowski, Deyu Hu, Thorsten von Eicken
1998 — conf
Resource management for extensible Internet servers.
ACM SIGOPS European Workshop
Grzegorz Czajkowski, Chi-Chao Chang, Chris Hawblitzel, Deyu Hu, Thorsten von Eicken
1998 — conf
Security versus performance tradeoffs in RPC implementations for safe language systems.
ACM SIGOPS European Workshop
Chi-Chao Chang, Grzegorz Czajkowski, Chris Hawblitzel, Deyu Hu, Thorsten von Eicken
1998 — conf
The Mobile Object Layer: A Run-Time Substrate for Mobile Adaptive Computations.
ISCOPE
Nikos Chrisochoides, Kevin J. Barker, Démian Nave, Chris Hawblitzel
1996 A conf
Low-Latency Communication on the IBM RISC System/6000 SP.
SC
Chi-Chao Chang, Grzegorz Czajkowski, Chris Hawblitzel, Thorsten von Eicken