Chris Hawblitzel

Publication Activity (10 Years)

Years Active: 1996-2024
Publications (10 Years): 16

Top Topics

Inference Control

Distributed Systems

Concurrent Programs

Top Venues

Proc. ACM Program. Lang.

Publications

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