Chris Hawblitzel

According to our database, Chris Hawblitzel authored at least 46 papers between 1996 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

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, Ziqiao Zhou, Shan Lu

CoRR, 2024

Verus: A Practical Foundation for Systems Verification.

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

Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, 2024

VeriSMo: A Verified Security Module for Confidential VMs.

Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, Weidong Cui

Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation, 2024

2023

Verus: Verifying Rust Programs using Linear Ghost Types.

Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel

Proc. ACM Program. Lang., April, 2023

Verus: Verifying Rust Programs using Linear Ghost Types (extended version).

Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel

CoRR, 2023

Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems.

Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, Bryan Parno

Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation, 2023

2022

Linear types for large-scale systems verification.

Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, Chris Hawblitzel

Proc. ACM Program. Lang., 2022

2020

Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language.

Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel

Proceedings of the Software Verification - 12th International Conference, 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, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella Béguelin

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

Storage Systems are Distributed Systems (So Verify Them That Way!).

Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, Bryan Parno

Proceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation, 2020

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

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, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella Béguelin

IACR Cryptol. ePrint Arch., 2019

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, Nikhil Swamy

Proceedings of the Programming Languages and Systems, 2019

2018

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, Nikhil Swamy

CoRR, 2018

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

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

Proceedings of the 26th USENIX Security Symposium, 2017

Komodo: Using verification to disentangle secure-enclave hardware from software.

Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, Bryan Parno

Proceedings of the 26th Symposium on Operating Systems Principles, 2017

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, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella Béguelin, Jean Karim Zinzindohoue

Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

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

Proceedings of the 25th Symposium on Operating Systems Principles, 2015

Automatic Rootcausing for Program Equivalence Failures in Binaries.

Shuvendu K. Lahiri, Rohit Sinha, Chris Hawblitzel

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Automated and Modular Refinement Reasoning for Concurrent Programs.

Chris Hawblitzel, Erez Petrank, Shaz Qadeer, Serdar Tasiran

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

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

Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, 2014

Cosh: Clear OS Data Sharing In An Incoherent World.

Andrew Baumann, Chris Hawblitzel, Kornilios Kourtis, Tim Harris, Timothy Roscoe

Proceedings of the 2014 Conference on Timely Results in Operating Systems, 2014

2013

Differential assertion checking.

Shuvendu K. Lahiri, Kenneth L. McMillan, Rahul Sharma, Chris Hawblitzel

Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 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

Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2013

Towards Modularly Comparing Programs Using Automated Theorem Provers.

Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, Henrique Rebêlo

Proceedings of the Automated Deduction - CADE-24, 2013

2012

SYMDIFF: A Language-Agnostic Semantic Diff Tool for Imperative Programs.

Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Rebêlo

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

Safe to the last instruction: automated verification of a type-safe operating system.

Jean Yang, Chris Hawblitzel

Commun. ACM, 2011

Type safety from the ground up.

Chris Hawblitzel

Proceedings of TLDI 2011: 2011 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2011

2010

Automated Verification of Practical Garbage Collectors

Chris Hawblitzel, Erez Petrank

Log. Methods Comput. Sci., 2010

Inferable object-oriented typed assembly language.

Ross Tate, Juan Chen, Chris Hawblitzel

Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2010

2009

Helios: heterogeneous multiprocessing with satellite kernels.

Edmund B. Nightingale, Orion Hodson, Ross McIlroy, Chris Hawblitzel, Galen C. Hunt

Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009

2008

Type-preserving compilation for large-scale optimizing object-oriented compilers.

Juan Chen, Chris Hawblitzel, Frances Perry, Michael Emmi, Jeremy Condit, Derrick Coetzee, Polyvios Pratikakis

Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, 2008

2007

A garbage-collecting typed assembly language.

Chris Hawblitzel, Heng Huang, Lea Wittie, Juan Chen

Proceedings of TLDI'07: 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2007

Checking the hardware-software interface in spec#.

Kevin Bierhoff, Chris Hawblitzel

Proceedings of the 4th workshop on Programming languages and operating systems, 2007

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

Proceedings of the 2007 EuroSys Conference, Lisbon, Portugal, March 21-23, 2007, 2007

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

Proceedings of the 2006 EuroSys Conference, Leuven, Belgium, April 18-21, 2006, 2006

Deconstructing process isolation.

Mark Aiken, Manuel Fähndrich, Chris Hawblitzel, Galen C. Hunt, James R. Larus

Proceedings of the 2006 workshop on Memory System Performance and Correctness, 2006

2002

Luna: A Flexible Java Protection System.

Chris Hawblitzel, Thorsten von Eicken

Proceedings of the 5th Symposium on Operating System Design and Implementation (OSDI 2002), 2002

2000

Adding Operating System Structure to Language-Based Protection.

Chris Hawblitzel

PhD thesis, 2000

1999

J-Kernel: A Capability-Based Operating System for Java.

Thorsten von Eicken, Chi-Chao Chang, Grzegorz Czajkowski, Chris Hawblitzel, Deyu Hu, Dan Spoonhower

Proceedings of the Secure Internet Programming, 1999

1998

Implementing Multiple Protection Domains in Java.

Chris Hawblitzel, Chi-Chao Chang, Grzegorz Czajkowski, Deyu Hu, Thorsten von Eicken

Proceedings of the 1998 USENIX Annual Technical Conference, 1998

Resource management for extensible Internet servers.

Grzegorz Czajkowski, Chi-Chao Chang, Chris Hawblitzel, Deyu Hu, Thorsten von Eicken

Proceedings of the 8th ACM SIGOPS European Workshop: Support for Composing Distributed Applications, 1998

Security versus performance tradeoffs in RPC implementations for safe language systems.

Chi-Chao Chang, Grzegorz Czajkowski, Chris Hawblitzel, Deyu Hu, Thorsten von Eicken

Proceedings of the 8th ACM SIGOPS European Workshop: Support for Composing Distributed Applications, 1998

The Mobile Object Layer: A Run-Time Substrate for Mobile Adaptive Computations.

Nikos Chrisochoides, Kevin J. Barker, Démian Nave, Chris Hawblitzel

Proceedings of the Computing in Object-Oriented Parallel Environments, 1998

1996

Low-Latency Communication on the IBM RISC System/6000 SP.

Chi-Chao Chang, Grzegorz Czajkowski, Chris Hawblitzel, Thorsten von Eicken

Proceedings of the 1996 ACM/IEEE Conference on Supercomputing, 1996