Jay Lorch

Senior Principal Researcher

Publications

View by:

- VeruSAGE-Bench: A Benchmark Suite for Rust System Verification
  
  Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jacob R Lorch, Shan Lu
  
  2026 NeurIPS | December 2026
  
  Publication
- From Lab to Fleet: Building and Deploying a Practical Rowhammer Defense in Cloud SoCs
  
  Stefan Saroiu, Sujay Yadalam, Alec Wolman, Will Remaklus, Daniel S. Berger, Isaac H. Luna, Ishwar Agarwal, Jacob R Lorch
  
  International Symposium on Computer Architecture | June 2026
  
  Publication Project
- Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
  
  Nongyu Di, Tianyu Chen, Shan Lu, Shuai Lu, Yeyun Gong, Peng Cheng, Jacob R Lorch, Yuan Yao, Xiaoxing Ma
  
  February 2026
  
  February 2026
  
  Publication Project
- VeruSAGE: A Study of Agent-Based Verification for Rust Systems
  
  Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jacob R Lorch, Shan Lu
  
  December 2025
  
  December 2025
  
  Preprint Github Project
- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github Project
- 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
  
  USENIX Symposium on Operating Systems Design and Implementation (OSDI) | July 2025
  
  Distinguished Artifact Award
  
  Publication Project
- 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
  
  Symposium on Operating Systems Principles | November 2024
  
  Distinguished Artifact Award
  
  Publication Project
- Armada: Low-Effort Verification of High-Performance Concurrent Programs
  
  Jacob R Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, Xueyuan Zhao
  
  International Conference on Programming Language Design and Implementation (PLDI) | June 2020
  
  Distinguished Paper Award
  
  Publication Project
- Capturing and Enhancing In Situ System Observability for Failure Detection
  
  Peng Huang (pehuan), Chuanxiong Guo, Jacob R. Lorch (lorch), Lidong Zhou, Yingnong Dang
  
  Operating Systems Design and Implementation (OSDI) | October 2018
  
  Publication
- Vale: Verifying High-Performance Cryptographic Assembly Code
  
  Barry Bond, Chris Hawblitzel, Manos Kapritsos, Rustan Leino, Jacob R Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson
  
  Proceedings of the USENIX Security Symposium | August 2017
  
  Distinguished Paper Award
  
  Publication Access Github Project
- IronFleet: Proving Safety and Liveness of Practical Distributed Systems
  
  Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
  
  Communications of the ACM | July 2017, Vol 60
  
  CACM Research Highlight
  
  Publication Project
- Gray Failure: The Achilles’ Heel of Cloud-Scale Systems
  
  Ryan Huang, Chuanxiong Guo, Lidong Zhou, Jacob R Lorch, Yingnong Dang, Murali Chintalapati, Randolph Yao
  
  Proceedings of the ACM Workshop on Hot Topics in Operating Systems (HotOS) | May 2017
  
  PDF Project
- 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, Rustan Leino, Jacob R Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
  
  SNAPL 2017 - 2nd Summit on Advances in Programming Languages | May 2017
  
  PDF Publication Publication Project
- Realizing the fault-tolerance promise of cloud storage using locks with intent
  
  Srinath Setty, Chunzhi Su, Jay Lorch, Lidong Zhou, Hao Chen, Parveen Patel, Jinglei Ren
  
  Operating Systems Design and Implementation (OSDI) | November 2016
  
  PDF
- IronFleet: Proving Practical Distributed Systems Correct
  
  Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
  
  Proceedings of the ACM Symposium on Operating Systems Principles (SOSP) | October 2015
  
  PDF Project
- Tardigrade: Leveraging Lightweight Virtual Machines to Easily and Efficiently Construct Fault-Tolerant Services
  
  Jacob R Lorch, Andrew Baumann, Lisa Glendenning, Dutch T. Meyer, Andrew Warfield
  
  12th USENIX Symposium on Networked Systems Design and Implementation (NSDI'15) | May 2015
  
  PDF Publication Project
- 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
  
  USENIX Symposium on Operating Systems Design and Implementation (OSDI) | October 2014
  
  PDF Github Project Project
- Zero-Effort Payments: Design, Deployment, and Lessons
  
  Christopher Smowton, Jacob R Lorch, David Molnar, Stefan Saroiu, Alec Wolman
  
  Proceedings of the ACM International Joint Conference on Pervasive and Ubiquitous Computing (UbiComp) | September 2014
  
  Proceedings of the ACM International Joint Conference on Pervasive and Ubiquitous Computing (UbiComp)
  
  PDF Publication Project
- Composing OS extensions safely and efficiently with Bascule
  
  Andrew Baumann, Dongyoon Lee, Pedro Fonseca, Lisa Glendenning, Jacob R Lorch, Barry Bond, Reuben Olinsky, Galen Hunt
  
  Eurosys | April 2013
  
  PDF Project Project
- Seamless Customer Identification
  
  Christopher Smowton, Jacob R Lorch, David Molnar, Stefan Saroiu, Alec Wolman
  
  MSR-TR-2013-31 | March 2013
  
  PDF Project
- Shroud: Enabling Private Access to Large-Scale Data in the Data Center
  
  Jacob R Lorch, Bryan Parno, James Mickens, Mariana Raykova, Joshua Schiffman
  
  Proceedings of the 11th USENIX Conference on File and Storage Technologies (FAST) | February 2013
  
  Proceedings of the 11th USENIX Conference on File and Storage Technologies (FAST)
  
  PDF
- Don’t Lose Sleep Over Availability: The GreenUp Decentralized Wakeup Service
  
  Siddhartha Sen, Jacob R. Lorch, Richard Hughes, Carlos Garcia Jurado Suarez, Brian Zill, Weverton Cordeiro, Jitendra Padhye, Jacob R Lorch, Jitu Padhye
  
  Proceedings of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI) | April 2012
  
  Proceedings of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI)
  
  PDF Project
- GreenUp: A Decentralized System for Making Sleeping Machines Available
  
  Siddhartha Sen, Jacob R Lorch, Richard Hughes, Carlos Garcia, Brian Zill, Weverton Cordeiro, Jitu Padhye
  
  MSR-TR-2012-21 | March 2012
  
  PDF
- Enabling Security in Cloud Storage SLAs with CloudProof
  
  Raluca Ada Popa, Jacob R. Lorch, David Molnar, Helen Wang, Li Zhuang, Jacob R Lorch
  
  USENIX Annual Technical Conference | June 2011
  
  PDF
- Memoir: Practical State Continuity for Protected Modules
  
  Bryan Parno, Jacob R Lorch, John (JD) Douceur, James Mickens, Jonathan M. McCune
  
  Proceedings of the IEEE Symposium on Security and Privacy | May 2011
  
  Proceedings of the IEEE Symposium on Security and Privacy
  
  PDF
- Memoir—Formal Specs and Correctness Proofs
  
  John (JD) Douceur, Jacob R Lorch, Bryan Parno, James Mickens, Jonathan M. McCune
  
  MSR-TR-2011-19 | February 2011
  
  PDF PDF
- The Utility Coprocessor: Massively Parallel Computation from the Coffee Shop
  
  Jeremy Elson, Jon Howell, Jacob R Lorch, John (JD) Douceur
  
  Proceedings of the 2010 USENIX Annual Technical Conference | June 2010
  
  Proceedings of the 2010 USENIX Annual Technical Conference
  
  PDF
- Enabling Security in Cloud Storage SLAs with CloudProof
  
  David Molnar, Jacob R Lorch, Helen Wang, Raluca Ada Popa, Li Zhuang
  
  MSR-TR-2010-46 | May 2010
  
  PDF
- Crom: Faster Web Browsing Using Speculative Execution
  
  James Mickens, Jeremy Elson, Jon Howell, Jacob R Lorch
  
  Proceedings of NSDI | April 2010
  
  PDF
- Matchmaking for online games and other latency-sensitive P2P systems
  
  Sharad Agarwal, Jacob R Lorch
  
  SIGCOMM | August 2009
  
  Publication Publication
- TrInc: Small Trusted Hardware for Large Distributed Systems
  
  Dave Levin, John (JD) Douceur, Jacob R Lorch, Thomas Moscibroda
  
  Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI) | April 2009
  
  NSDI Best Paper Award
  
  Publication
- Leveraging legacy code to deploy desktop applications on the Web
  
  John (JD) Douceur, Jeremy Elson, Jon Howell, Jacob R Lorch
  
  Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI) | December 2008
  
  PDF Project
- Donnybrook: Enabling Large-Scale, High-Speed, Peer-to-Peer Games
  
  Ashwin Bharambe, John (JD) Douceur, Jacob R Lorch, Thomas Moscibroda, Jeffrey Pang, Srinivasan Seshan, Xinyu Zhuang
  
  SIGCOMM 2008: ACM SIGCOMM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, Seattle, WA | August 2008
  
  PDF
- A five-year study of file-system metadata
  
  Nitin Agrawal, Bill Bolosky, John (JD) Douceur, Jacob R Lorch
  
  Proceedings of the 5th USENIX Conference on File and Storage Technologies (FAST) | October 2007
  
  FAST ’21 USENIX Test of Time Award
  
  PDF Publication
- Enhancing game-server AI with distributed client computation
  
  Jacob R Lorch, Frank Uyeda, Randall C. Wood, John (JD) Douceur
  
  Proceedings of the 17th International Workshop on Network and Operating Systems Support for Digital Audio and Video (NOSSDAV) | June 2007
  
  Proceedings of the 17th International Workshop on Network and Operating Systems Support for Digital Audio and Video (NOSSDAV)
  
  PDF
- Maximizing Total Upload in Latency-Sensitive P2P Applications
  
  John (JD) Douceur, Jacob R Lorch, Thomas Moscibroda
  
  SPAA 2007: 19th ACM Symposium on Parallelism in Algorithms and Architectures, San Diego, California, USA | June 2007
  
  PDF
- SAV-V: Securing Anti-Virus with Virtualization
  
  Jacob R Lorch, Bryan Parno, Helen Wang
  
  MSR-TR-2011-101 | April 2007
  
  PDF
- Scaling peer-to-peer games in low-bandwidth environments
  
  Jeffrey Pang, Frank Uyeda, Jacob R Lorch
  
  Proceedings of the 6th International Workshop on Peer-to-Peer Systems (IPTPS) | February 2007
  
  PDF
- SubVirt: Implementing malware with virtual machines
  
  Samuel T. King, Peter M. Chen, Yi-Min Wang, Chad Verbowski, Helen Wang, Jacob R Lorch
  
  Proceedings of the 2006 IEEE Symposium on Security and Privacy | May 2006
  
  PDF
- The SMART way to migrate replicated stateful services
  
  Jacob R. Lorch, Atul Adya, William J. Bolosky, Ronnie Chaiken, John R. Douceur, Jon Howell, John (JD) Douceur, Jacob R Lorch, Bill Bolosky
  
  Proceedings of the 2006 EuroSys Conference | April 2006
  
  PDF
- Load Management in a Large-Scale Decentralized File System
  
  Atul Adya, Bill Bolosky, Ronnie Chaiken, John (JD) Douceur, Jon Howell, Jacob R Lorch
  
  MSR-TR-2004-60 | July 2004
  
  PDF
- PACE: A new approach to dynamic voltage scaling
  
  Jacob R. Lorch, Alan Jay Smith, Jacob R Lorch
  
  IEEE Transactions on Computers | July 2004, Vol 53: pp. 856-869
  
  PDF
- Correctness of Paxos with Replica-Set-Specific Views
  
  Jon Howell, Jacob R Lorch, John (JD) Douceur
  
  MSR-TR-2004-45 | June 2004
  
  PDF PDF
- Using user interface event information in dynamic voltage scaling algorithms
  
  Jacob R. Lorch, Alan Jay Smith, Jacob R Lorch
  
  Proceedings of the 11th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS) | October 2003
  
  Proceedings of the 11th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS)
  
  PDF
- Operating system modifications for task-based speed and voltage scheduling
  
  Jacob R Lorch, Alan Jay Smith
  
  Proceedings of the First International Conference on Mobile Systems, Applications, and Services (MobiSys) | May 2003
  
  PDF
- FARSITE: Federated, available, and reliable storage for an incompletely trusted environment
  
  Atul Adya, Bill Bolosky, Miguel Castro, Ronnie Chaiken, Gerald Cermak, John (JD) Douceur, Jon Howell, Jacob R Lorch, Marvin Theimer, Roger Wattenhofer,
  
  Proceedings of the 5th Symposium on Operating Systems Design and Implementation (OSDI) | December 2002
  
  Proceedings of the 5th Symposium on Operating Systems Design and Implementation (OSDI)
  
  PDF
- Improving dynamic voltage scaling algorithms with PACE
  
  Jacob R Lorch, Alan Jay Smith
  
  Proceedings of the ACM SIGMETRICS 2001 Conference | June 2001
  
  PDF
- Operating systems techniques for reducing processor energy consumption
  
  Jacob R Lorch
  
  December 2001
  
  December 2001
  
  PDF
- The VTrace tool: building a system tracer for Windows NT and Windows 2000
  
  Jacob R. Lorch, Alan Jay Smith, Jacob R Lorch
  
  MSDN Magazine | October 2000, Vol 15(10): pp. 86-102
  
  Publication
- A comparison of file system workloads
  
  Drew Roselli, Jacob R. Lorch, Thomas E. Anderson, Jacob R Lorch
  
  Proceedings of the 2000 USENIX Annual Technical Conference | June 2000
  
  Proceedings of the 2000 USENIX Annual Technical Conference
  
  PDF
- Energy consumption of Apple Macintosh computers
  
  Jacob R. Lorch, Alan Jay Smith, Jacob R Lorch
  
  IEEE Micro | November 1998, Vol 18: pp. 54-63
  
  PDF
- Software Strategies for Portable Computer Energy Management
  
  Jacob R Lorch, Alan Jay Smith
  
  IEEE Personal Communications Magazine | June 1998, pp. 60-73
  
  PDF
- Scheduling techniques for reducing processor energy use in MacOS
  
  Jacob R Lorch, Alan Jay Smith
  
  Wireless Networks | October 1997, pp. 311-324
  
  PDF
- Reducing Processor Power Consumption by Improving Processor Time Management in a Single-User Operating System
  
  Jacob R Lorch, Alan Jay Smith
  
  Proceedings of the Second ACM International Conference on Mobile Computing and Networking (MOBICOM) | November 1996
  
  PDF
- Making World Wide Web caching servers cooperate
  
  Radhika Malpani, Jacob R Lorch, David Berger
  
  Proceedings of the Fourth International World Wide Web Conference | December 1995
  
  Proceedings of the Fourth International World Wide Web Conference
  
  Publication

- VeruSAGE-Bench: A Benchmark Suite for Rust System Verification
  
  Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jacob R Lorch, Shan Lu
  
  2026 NeurIPS | December 2026
  
  Publication
- Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
  
  Nongyu Di, Tianyu Chen, Shan Lu, Shuai Lu, Yeyun Gong, Peng Cheng, Jacob R Lorch, Yuan Yao, Xiaoxing Ma
  
  February 2026
  
  February 2026
  
  Publication Project
- VeruSAGE: A Study of Agent-Based Verification for Rust Systems
  
  Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jacob R Lorch, Shan Lu
  
  December 2025
  
  December 2025
  
  Preprint Github Project
- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github Project
- Seamless Customer Identification
  
  Christopher Smowton, Jacob R Lorch, David Molnar, Stefan Saroiu, Alec Wolman
  
  MSR-TR-2013-31 | March 2013
  
  PDF Project
- Improving dynamic voltage scaling algorithms with PACE
  
  Jacob R Lorch, Alan Jay Smith
  
  Proceedings of the ACM SIGMETRICS 2001 Conference | June 2001
  
  PDF
- A comparison of file system workloads
  
  Drew Roselli, Jacob R. Lorch, Thomas E. Anderson, Jacob R Lorch
  
  Proceedings of the 2000 USENIX Annual Technical Conference | June 2000
  
  Proceedings of the 2000 USENIX Annual Technical Conference
  
  PDF
- Energy consumption of Apple Macintosh computers
  
  Jacob R. Lorch, Alan Jay Smith, Jacob R Lorch
  
  IEEE Micro | November 1998, Vol 18: pp. 54-63
  
  PDF
- Software Strategies for Portable Computer Energy Management
  
  Jacob R Lorch, Alan Jay Smith
  
  IEEE Personal Communications Magazine | June 1998, pp. 60-73
  
  PDF
- Scheduling techniques for reducing processor energy use in MacOS
  
  Jacob R Lorch, Alan Jay Smith
  
  Wireless Networks | October 1997, pp. 311-324
  
  PDF
- Reducing Processor Power Consumption by Improving Processor Time Management in a Single-User Operating System
  
  Jacob R Lorch, Alan Jay Smith
  
  Proceedings of the Second ACM International Conference on Mobile Computing and Networking (MOBICOM) | November 1996
  
  PDF
- Making World Wide Web caching servers cooperate
  
  Radhika Malpani, Jacob R Lorch, David Berger
  
  Proceedings of the Fourth International World Wide Web Conference | December 1995
  
  Proceedings of the Fourth International World Wide Web Conference
  
  Publication
- VeruSAGE-Bench: A Benchmark Suite for Rust System Verification
  
  Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jacob R Lorch, Shan Lu
  
  2026 NeurIPS | December 2026
  
  Publication
- From Lab to Fleet: Building and Deploying a Practical Rowhammer Defense in Cloud SoCs
  
  Stefan Saroiu, Sujay Yadalam, Alec Wolman, Will Remaklus, Daniel S. Berger, Isaac H. Luna, Ishwar Agarwal, Jacob R Lorch
  
  International Symposium on Computer Architecture | June 2026
  
  Publication Project
- Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
  
  Nongyu Di, Tianyu Chen, Shan Lu, Shuai Lu, Yeyun Gong, Peng Cheng, Jacob R Lorch, Yuan Yao, Xiaoxing Ma
  
  February 2026
  
  February 2026
  
  Publication Project
- VeruSAGE: A Study of Agent-Based Verification for Rust Systems
  
  Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jacob R Lorch, Shan Lu
  
  December 2025
  
  December 2025
  
  Preprint Github Project
- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github Project
- 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
  
  USENIX Symposium on Operating Systems Design and Implementation (OSDI) | July 2025
  
  Distinguished Artifact Award
  
  Publication Project
- 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
  
  Symposium on Operating Systems Principles | November 2024
  
  Distinguished Artifact Award
  
  Publication Project
- Armada: Low-Effort Verification of High-Performance Concurrent Programs
  
  Jacob R Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, Xueyuan Zhao
  
  International Conference on Programming Language Design and Implementation (PLDI) | June 2020
  
  Distinguished Paper Award
  
  Publication Project
- Capturing and Enhancing In Situ System Observability for Failure Detection
  
  Peng Huang (pehuan), Chuanxiong Guo, Jacob R. Lorch (lorch), Lidong Zhou, Yingnong Dang
  
  Operating Systems Design and Implementation (OSDI) | October 2018
  
  Publication
- IronFleet: Proving Safety and Liveness of Practical Distributed Systems
  
  Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
  
  Communications of the ACM | July 2017, Vol 60
  
  CACM Research Highlight
  
  Publication Project
- Gray Failure: The Achilles’ Heel of Cloud-Scale Systems
  
  Ryan Huang, Chuanxiong Guo, Lidong Zhou, Jacob R Lorch, Yingnong Dang, Murali Chintalapati, Randolph Yao
  
  Proceedings of the ACM Workshop on Hot Topics in Operating Systems (HotOS) | May 2017
  
  PDF Project
- Realizing the fault-tolerance promise of cloud storage using locks with intent
  
  Srinath Setty, Chunzhi Su, Jay Lorch, Lidong Zhou, Hao Chen, Parveen Patel, Jinglei Ren
  
  Operating Systems Design and Implementation (OSDI) | November 2016
  
  PDF
- IronFleet: Proving Practical Distributed Systems Correct
  
  Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
  
  Proceedings of the ACM Symposium on Operating Systems Principles (SOSP) | October 2015
  
  PDF Project
- Tardigrade: Leveraging Lightweight Virtual Machines to Easily and Efficiently Construct Fault-Tolerant Services
  
  Jacob R Lorch, Andrew Baumann, Lisa Glendenning, Dutch T. Meyer, Andrew Warfield
  
  12th USENIX Symposium on Networked Systems Design and Implementation (NSDI'15) | May 2015
  
  PDF Publication Project
- 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
  
  USENIX Symposium on Operating Systems Design and Implementation (OSDI) | October 2014
  
  PDF Github Project Project
- Composing OS extensions safely and efficiently with Bascule
  
  Andrew Baumann, Dongyoon Lee, Pedro Fonseca, Lisa Glendenning, Jacob R Lorch, Barry Bond, Reuben Olinsky, Galen Hunt
  
  Eurosys | April 2013
  
  PDF Project Project
- Seamless Customer Identification
  
  Christopher Smowton, Jacob R Lorch, David Molnar, Stefan Saroiu, Alec Wolman
  
  MSR-TR-2013-31 | March 2013
  
  PDF Project
- Don’t Lose Sleep Over Availability: The GreenUp Decentralized Wakeup Service
  
  Siddhartha Sen, Jacob R. Lorch, Richard Hughes, Carlos Garcia Jurado Suarez, Brian Zill, Weverton Cordeiro, Jitendra Padhye, Jacob R Lorch, Jitu Padhye
  
  Proceedings of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI) | April 2012
  
  Proceedings of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI)
  
  PDF Project
- GreenUp: A Decentralized System for Making Sleeping Machines Available
  
  Siddhartha Sen, Jacob R Lorch, Richard Hughes, Carlos Garcia, Brian Zill, Weverton Cordeiro, Jitu Padhye
  
  MSR-TR-2012-21 | March 2012
  
  PDF
- Enabling Security in Cloud Storage SLAs with CloudProof
  
  Raluca Ada Popa, Jacob R. Lorch, David Molnar, Helen Wang, Li Zhuang, Jacob R Lorch
  
  USENIX Annual Technical Conference | June 2011
  
  PDF
- Memoir: Practical State Continuity for Protected Modules
  
  Bryan Parno, Jacob R Lorch, John (JD) Douceur, James Mickens, Jonathan M. McCune
  
  Proceedings of the IEEE Symposium on Security and Privacy | May 2011
  
  Proceedings of the IEEE Symposium on Security and Privacy
  
  PDF
- Memoir—Formal Specs and Correctness Proofs
  
  John (JD) Douceur, Jacob R Lorch, Bryan Parno, James Mickens, Jonathan M. McCune
  
  MSR-TR-2011-19 | February 2011
  
  PDF PDF
- The Utility Coprocessor: Massively Parallel Computation from the Coffee Shop
  
  Jeremy Elson, Jon Howell, Jacob R Lorch, John (JD) Douceur
  
  Proceedings of the 2010 USENIX Annual Technical Conference | June 2010
  
  Proceedings of the 2010 USENIX Annual Technical Conference
  
  PDF
- Enabling Security in Cloud Storage SLAs with CloudProof
  
  David Molnar, Jacob R Lorch, Helen Wang, Raluca Ada Popa, Li Zhuang
  
  MSR-TR-2010-46 | May 2010
  
  PDF
- Crom: Faster Web Browsing Using Speculative Execution
  
  James Mickens, Jeremy Elson, Jon Howell, Jacob R Lorch
  
  Proceedings of NSDI | April 2010
  
  PDF
- Matchmaking for online games and other latency-sensitive P2P systems
  
  Sharad Agarwal, Jacob R Lorch
  
  SIGCOMM | August 2009
  
  Publication Publication
- TrInc: Small Trusted Hardware for Large Distributed Systems
  
  Dave Levin, John (JD) Douceur, Jacob R Lorch, Thomas Moscibroda
  
  Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI) | April 2009
  
  NSDI Best Paper Award
  
  Publication
- Donnybrook: Enabling Large-Scale, High-Speed, Peer-to-Peer Games
  
  Ashwin Bharambe, John (JD) Douceur, Jacob R Lorch, Thomas Moscibroda, Jeffrey Pang, Srinivasan Seshan, Xinyu Zhuang
  
  SIGCOMM 2008: ACM SIGCOMM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, Seattle, WA | August 2008
  
  PDF
- Enhancing game-server AI with distributed client computation
  
  Jacob R Lorch, Frank Uyeda, Randall C. Wood, John (JD) Douceur
  
  Proceedings of the 17th International Workshop on Network and Operating Systems Support for Digital Audio and Video (NOSSDAV) | June 2007
  
  Proceedings of the 17th International Workshop on Network and Operating Systems Support for Digital Audio and Video (NOSSDAV)
  
  PDF
- Maximizing Total Upload in Latency-Sensitive P2P Applications
  
  John (JD) Douceur, Jacob R Lorch, Thomas Moscibroda
  
  SPAA 2007: 19th ACM Symposium on Parallelism in Algorithms and Architectures, San Diego, California, USA | June 2007
  
  PDF
- Scaling peer-to-peer games in low-bandwidth environments
  
  Jeffrey Pang, Frank Uyeda, Jacob R Lorch
  
  Proceedings of the 6th International Workshop on Peer-to-Peer Systems (IPTPS) | February 2007
  
  PDF
- SubVirt: Implementing malware with virtual machines
  
  Samuel T. King, Peter M. Chen, Yi-Min Wang, Chad Verbowski, Helen Wang, Jacob R Lorch
  
  Proceedings of the 2006 IEEE Symposium on Security and Privacy | May 2006
  
  PDF
- Load Management in a Large-Scale Decentralized File System
  
  Atul Adya, Bill Bolosky, Ronnie Chaiken, John (JD) Douceur, Jon Howell, Jacob R Lorch
  
  MSR-TR-2004-60 | July 2004
  
  PDF
- PACE: A new approach to dynamic voltage scaling
  
  Jacob R. Lorch, Alan Jay Smith, Jacob R Lorch
  
  IEEE Transactions on Computers | July 2004, Vol 53: pp. 856-869
  
  PDF
- Correctness of Paxos with Replica-Set-Specific Views
  
  Jon Howell, Jacob R Lorch, John (JD) Douceur
  
  MSR-TR-2004-45 | June 2004
  
  PDF PDF
- Operating system modifications for task-based speed and voltage scheduling
  
  Jacob R Lorch, Alan Jay Smith
  
  Proceedings of the First International Conference on Mobile Systems, Applications, and Services (MobiSys) | May 2003
  
  PDF
- FARSITE: Federated, available, and reliable storage for an incompletely trusted environment
  
  Atul Adya, Bill Bolosky, Miguel Castro, Ronnie Chaiken, Gerald Cermak, John (JD) Douceur, Jon Howell, Jacob R Lorch, Marvin Theimer, Roger Wattenhofer,
  
  Proceedings of the 5th Symposium on Operating Systems Design and Implementation (OSDI) | December 2002
  
  Proceedings of the 5th Symposium on Operating Systems Design and Implementation (OSDI)
  
  PDF
- Operating systems techniques for reducing processor energy consumption
  
  Jacob R Lorch
  
  December 2001
  
  December 2001
  
  PDF
- From Lab to Fleet: Building and Deploying a Practical Rowhammer Defense in Cloud SoCs
  
  Stefan Saroiu, Sujay Yadalam, Alec Wolman, Will Remaklus, Daniel S. Berger, Isaac H. Luna, Ishwar Agarwal, Jacob R Lorch
  
  International Symposium on Computer Architecture | June 2026
  
  Publication Project
- Vale: Verifying High-Performance Cryptographic Assembly Code
  
  Barry Bond, Chris Hawblitzel, Manos Kapritsos, Rustan Leino, Jacob R Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson
  
  Proceedings of the USENIX Security Symposium | August 2017
  
  Distinguished Paper Award
  
  Publication Access Github Project
- 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, Rustan Leino, Jacob R Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
  
  SNAPL 2017 - 2nd Summit on Advances in Programming Languages | May 2017
  
  PDF Publication Publication Project
- IronFleet: Proving Practical Distributed Systems Correct
  
  Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
  
  Proceedings of the ACM Symposium on Operating Systems Principles (SOSP) | October 2015
  
  PDF Project
- 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
  
  USENIX Symposium on Operating Systems Design and Implementation (OSDI) | October 2014
  
  PDF Github Project Project
- Zero-Effort Payments: Design, Deployment, and Lessons
  
  Christopher Smowton, Jacob R Lorch, David Molnar, Stefan Saroiu, Alec Wolman
  
  Proceedings of the ACM International Joint Conference on Pervasive and Ubiquitous Computing (UbiComp) | September 2014
  
  Proceedings of the ACM International Joint Conference on Pervasive and Ubiquitous Computing (UbiComp)
  
  PDF Publication Project
- Seamless Customer Identification
  
  Christopher Smowton, Jacob R Lorch, David Molnar, Stefan Saroiu, Alec Wolman
  
  MSR-TR-2013-31 | March 2013
  
  PDF Project
- Shroud: Enabling Private Access to Large-Scale Data in the Data Center
  
  Jacob R Lorch, Bryan Parno, James Mickens, Mariana Raykova, Joshua Schiffman
  
  Proceedings of the 11th USENIX Conference on File and Storage Technologies (FAST) | February 2013
  
  Proceedings of the 11th USENIX Conference on File and Storage Technologies (FAST)
  
  PDF
- Enabling Security in Cloud Storage SLAs with CloudProof
  
  Raluca Ada Popa, Jacob R. Lorch, David Molnar, Helen Wang, Li Zhuang, Jacob R Lorch
  
  USENIX Annual Technical Conference | June 2011
  
  PDF
- Memoir: Practical State Continuity for Protected Modules
  
  Bryan Parno, Jacob R Lorch, John (JD) Douceur, James Mickens, Jonathan M. McCune
  
  Proceedings of the IEEE Symposium on Security and Privacy | May 2011
  
  Proceedings of the IEEE Symposium on Security and Privacy
  
  PDF
- Memoir—Formal Specs and Correctness Proofs
  
  John (JD) Douceur, Jacob R Lorch, Bryan Parno, James Mickens, Jonathan M. McCune
  
  MSR-TR-2011-19 | February 2011
  
  PDF PDF
- SAV-V: Securing Anti-Virus with Virtualization
  
  Jacob R Lorch, Bryan Parno, Helen Wang
  
  MSR-TR-2011-101 | April 2007
  
  PDF
- SubVirt: Implementing malware with virtual machines
  
  Samuel T. King, Peter M. Chen, Yi-Min Wang, Chad Verbowski, Helen Wang, Jacob R Lorch
  
  Proceedings of the 2006 IEEE Symposium on Security and Privacy | May 2006
  
  PDF
- Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
  
  Nongyu Di, Tianyu Chen, Shan Lu, Shuai Lu, Yeyun Gong, Peng Cheng, Jacob R Lorch, Yuan Yao, Xiaoxing Ma
  
  February 2026
  
  February 2026
  
  Publication Project
- VeruSAGE: A Study of Agent-Based Verification for Rust Systems
  
  Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jacob R Lorch, Shan Lu
  
  December 2025
  
  December 2025
  
  Preprint Github Project
- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github Project
- 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
  
  USENIX Symposium on Operating Systems Design and Implementation (OSDI) | July 2025
  
  Distinguished Artifact Award
  
  Publication Project
- 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
  
  Symposium on Operating Systems Principles | November 2024
  
  Distinguished Artifact Award
  
  Publication Project
- Vale: Verifying High-Performance Cryptographic Assembly Code
  
  Barry Bond, Chris Hawblitzel, Manos Kapritsos, Rustan Leino, Jacob R Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson
  
  Proceedings of the USENIX Security Symposium | August 2017
  
  Distinguished Paper Award
  
  Publication Access Github Project
- IronFleet: Proving Safety and Liveness of Practical Distributed Systems
  
  Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
  
  Communications of the ACM | July 2017, Vol 60
  
  CACM Research Highlight
  
  Publication Project
- 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, Rustan Leino, Jacob R Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
  
  SNAPL 2017 - 2nd Summit on Advances in Programming Languages | May 2017
  
  PDF Publication Publication Project
- 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
  
  USENIX Symposium on Operating Systems Design and Implementation (OSDI) | October 2014
  
  PDF Github Project Project
- Leveraging legacy code to deploy desktop applications on the Web
  
  John (JD) Douceur, Jeremy Elson, Jon Howell, Jacob R Lorch
  
  Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI) | December 2008
  
  PDF Project
- Seamless Customer Identification
  
  Christopher Smowton, Jacob R Lorch, David Molnar, Stefan Saroiu, Alec Wolman
  
  MSR-TR-2013-31 | March 2013
  
  PDF Project
- Seamless Customer Identification
  
  Christopher Smowton, Jacob R Lorch, David Molnar, Stefan Saroiu, Alec Wolman
  
  MSR-TR-2013-31 | March 2013
  
  PDF Project
- Enabling Security in Cloud Storage SLAs with CloudProof
  
  Raluca Ada Popa, Jacob R. Lorch, David Molnar, Helen Wang, Li Zhuang, Jacob R Lorch
  
  USENIX Annual Technical Conference | June 2011
  
  PDF
- A five-year study of file-system metadata
  
  Nitin Agrawal, Bill Bolosky, John (JD) Douceur, Jacob R Lorch
  
  Proceedings of the 5th USENIX Conference on File and Storage Technologies (FAST) | October 2007
  
  FAST ’21 USENIX Test of Time Award
  
  PDF Publication
- The VTrace tool: building a system tracer for Windows NT and Windows 2000
  
  Jacob R. Lorch, Alan Jay Smith, Jacob R Lorch
  
  MSDN Magazine | October 2000, Vol 15(10): pp. 86-102
  
  Publication
- The SMART way to migrate replicated stateful services
  
  Jacob R. Lorch, Atul Adya, William J. Bolosky, Ronnie Chaiken, John R. Douceur, Jon Howell, John (JD) Douceur, Jacob R Lorch, Bill Bolosky
  
  Proceedings of the 2006 EuroSys Conference | April 2006
  
  PDF
- Using user interface event information in dynamic voltage scaling algorithms
  
  Jacob R. Lorch, Alan Jay Smith, Jacob R Lorch
  
  Proceedings of the 11th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS) | October 2003
  
  Proceedings of the 11th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS)
  
  PDF

- Improving dynamic voltage scaling algorithms with PACE
  
  Jacob R Lorch, Alan Jay Smith
  
  Proceedings of the ACM SIGMETRICS 2001 Conference | June 2001
  
  PDF
- A comparison of file system workloads
  
  Drew Roselli, Jacob R. Lorch, Thomas E. Anderson, Jacob R Lorch
  
  Proceedings of the 2000 USENIX Annual Technical Conference | June 2000
  
  Proceedings of the 2000 USENIX Annual Technical Conference
  
  PDF
- Reducing Processor Power Consumption by Improving Processor Time Management in a Single-User Operating System
  
  Jacob R Lorch, Alan Jay Smith
  
  Proceedings of the Second ACM International Conference on Mobile Computing and Networking (MOBICOM) | November 1996
  
  PDF
- Making World Wide Web caching servers cooperate
  
  Radhika Malpani, Jacob R Lorch, David Berger
  
  Proceedings of the Fourth International World Wide Web Conference | December 1995
  
  Proceedings of the Fourth International World Wide Web Conference
  
  Publication
- VeruSAGE-Bench: A Benchmark Suite for Rust System Verification
  
  Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jacob R Lorch, Shan Lu
  
  2026 NeurIPS | December 2026
  
  Publication
- From Lab to Fleet: Building and Deploying a Practical Rowhammer Defense in Cloud SoCs
  
  Stefan Saroiu, Sujay Yadalam, Alec Wolman, Will Remaklus, Daniel S. Berger, Isaac H. Luna, Ishwar Agarwal, Jacob R Lorch
  
  International Symposium on Computer Architecture | June 2026
  
  Publication Project
- AutoVerus: Automated Proof Generation for Rust Code
  
  Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu
  
  Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) | October 2025
  
  Distinguished Artifact Award
  
  Publication Github Project
- 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
  
  USENIX Symposium on Operating Systems Design and Implementation (OSDI) | July 2025
  
  Distinguished Artifact Award
  
  Publication Project
- 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
  
  Symposium on Operating Systems Principles | November 2024
  
  Distinguished Artifact Award
  
  Publication Project
- Armada: Low-Effort Verification of High-Performance Concurrent Programs
  
  Jacob R Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, Xueyuan Zhao
  
  International Conference on Programming Language Design and Implementation (PLDI) | June 2020
  
  Distinguished Paper Award
  
  Publication Project
- Capturing and Enhancing In Situ System Observability for Failure Detection
  
  Peng Huang (pehuan), Chuanxiong Guo, Jacob R. Lorch (lorch), Lidong Zhou, Yingnong Dang
  
  Operating Systems Design and Implementation (OSDI) | October 2018
  
  Publication
- Vale: Verifying High-Performance Cryptographic Assembly Code
  
  Barry Bond, Chris Hawblitzel, Manos Kapritsos, Rustan Leino, Jacob R Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson
  
  Proceedings of the USENIX Security Symposium | August 2017
  
  Distinguished Paper Award
  
  Publication Access Github Project
- Gray Failure: The Achilles’ Heel of Cloud-Scale Systems
  
  Ryan Huang, Chuanxiong Guo, Lidong Zhou, Jacob R Lorch, Yingnong Dang, Murali Chintalapati, Randolph Yao
  
  Proceedings of the ACM Workshop on Hot Topics in Operating Systems (HotOS) | May 2017
  
  PDF Project
- 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, Rustan Leino, Jacob R Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
  
  SNAPL 2017 - 2nd Summit on Advances in Programming Languages | May 2017
  
  PDF Publication Publication Project
- Realizing the fault-tolerance promise of cloud storage using locks with intent
  
  Srinath Setty, Chunzhi Su, Jay Lorch, Lidong Zhou, Hao Chen, Parveen Patel, Jinglei Ren
  
  Operating Systems Design and Implementation (OSDI) | November 2016
  
  PDF
- IronFleet: Proving Practical Distributed Systems Correct
  
  Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
  
  Proceedings of the ACM Symposium on Operating Systems Principles (SOSP) | October 2015
  
  PDF Project
- Tardigrade: Leveraging Lightweight Virtual Machines to Easily and Efficiently Construct Fault-Tolerant Services
  
  Jacob R Lorch, Andrew Baumann, Lisa Glendenning, Dutch T. Meyer, Andrew Warfield
  
  12th USENIX Symposium on Networked Systems Design and Implementation (NSDI'15) | May 2015
  
  PDF Publication Project
- 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
  
  USENIX Symposium on Operating Systems Design and Implementation (OSDI) | October 2014
  
  PDF Github Project Project
- Zero-Effort Payments: Design, Deployment, and Lessons
  
  Christopher Smowton, Jacob R Lorch, David Molnar, Stefan Saroiu, Alec Wolman
  
  Proceedings of the ACM International Joint Conference on Pervasive and Ubiquitous Computing (UbiComp) | September 2014
  
  Proceedings of the ACM International Joint Conference on Pervasive and Ubiquitous Computing (UbiComp)
  
  PDF Publication Project
- Composing OS extensions safely and efficiently with Bascule
  
  Andrew Baumann, Dongyoon Lee, Pedro Fonseca, Lisa Glendenning, Jacob R Lorch, Barry Bond, Reuben Olinsky, Galen Hunt
  
  Eurosys | April 2013
  
  PDF Project Project
- Shroud: Enabling Private Access to Large-Scale Data in the Data Center
  
  Jacob R Lorch, Bryan Parno, James Mickens, Mariana Raykova, Joshua Schiffman
  
  Proceedings of the 11th USENIX Conference on File and Storage Technologies (FAST) | February 2013
  
  Proceedings of the 11th USENIX Conference on File and Storage Technologies (FAST)
  
  PDF
- Don’t Lose Sleep Over Availability: The GreenUp Decentralized Wakeup Service
  
  Siddhartha Sen, Jacob R. Lorch, Richard Hughes, Carlos Garcia Jurado Suarez, Brian Zill, Weverton Cordeiro, Jitendra Padhye, Jacob R Lorch, Jitu Padhye
  
  Proceedings of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI) | April 2012
  
  Proceedings of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI)
  
  PDF Project
- Enabling Security in Cloud Storage SLAs with CloudProof
  
  Raluca Ada Popa, Jacob R. Lorch, David Molnar, Helen Wang, Li Zhuang, Jacob R Lorch
  
  USENIX Annual Technical Conference | June 2011
  
  PDF
- Memoir: Practical State Continuity for Protected Modules
  
  Bryan Parno, Jacob R Lorch, John (JD) Douceur, James Mickens, Jonathan M. McCune
  
  Proceedings of the IEEE Symposium on Security and Privacy | May 2011
  
  Proceedings of the IEEE Symposium on Security and Privacy
  
  PDF
- The Utility Coprocessor: Massively Parallel Computation from the Coffee Shop
  
  Jeremy Elson, Jon Howell, Jacob R Lorch, John (JD) Douceur
  
  Proceedings of the 2010 USENIX Annual Technical Conference | June 2010
  
  Proceedings of the 2010 USENIX Annual Technical Conference
  
  PDF
- Crom: Faster Web Browsing Using Speculative Execution
  
  James Mickens, Jeremy Elson, Jon Howell, Jacob R Lorch
  
  Proceedings of NSDI | April 2010
  
  PDF
- Matchmaking for online games and other latency-sensitive P2P systems
  
  Sharad Agarwal, Jacob R Lorch
  
  SIGCOMM | August 2009
  
  Publication Publication
- TrInc: Small Trusted Hardware for Large Distributed Systems
  
  Dave Levin, John (JD) Douceur, Jacob R Lorch, Thomas Moscibroda
  
  Proceedings of the 6th USENIX Symposium on Networked Systems Design and Implementation (NSDI) | April 2009
  
  NSDI Best Paper Award
  
  Publication
- Leveraging legacy code to deploy desktop applications on the Web
  
  John (JD) Douceur, Jeremy Elson, Jon Howell, Jacob R Lorch
  
  Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI) | December 2008
  
  PDF Project
- Donnybrook: Enabling Large-Scale, High-Speed, Peer-to-Peer Games
  
  Ashwin Bharambe, John (JD) Douceur, Jacob R Lorch, Thomas Moscibroda, Jeffrey Pang, Srinivasan Seshan, Xinyu Zhuang
  
  SIGCOMM 2008: ACM SIGCOMM Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, Seattle, WA | August 2008
  
  PDF
- A five-year study of file-system metadata
  
  Nitin Agrawal, Bill Bolosky, John (JD) Douceur, Jacob R Lorch
  
  Proceedings of the 5th USENIX Conference on File and Storage Technologies (FAST) | October 2007
  
  FAST ’21 USENIX Test of Time Award
  
  PDF Publication
- Enhancing game-server AI with distributed client computation
  
  Jacob R Lorch, Frank Uyeda, Randall C. Wood, John (JD) Douceur
  
  Proceedings of the 17th International Workshop on Network and Operating Systems Support for Digital Audio and Video (NOSSDAV) | June 2007
  
  Proceedings of the 17th International Workshop on Network and Operating Systems Support for Digital Audio and Video (NOSSDAV)
  
  PDF
- Maximizing Total Upload in Latency-Sensitive P2P Applications
  
  John (JD) Douceur, Jacob R Lorch, Thomas Moscibroda
  
  SPAA 2007: 19th ACM Symposium on Parallelism in Algorithms and Architectures, San Diego, California, USA | June 2007
  
  PDF
- Scaling peer-to-peer games in low-bandwidth environments
  
  Jeffrey Pang, Frank Uyeda, Jacob R Lorch
  
  Proceedings of the 6th International Workshop on Peer-to-Peer Systems (IPTPS) | February 2007
  
  PDF
- SubVirt: Implementing malware with virtual machines
  
  Samuel T. King, Peter M. Chen, Yi-Min Wang, Chad Verbowski, Helen Wang, Jacob R Lorch
  
  Proceedings of the 2006 IEEE Symposium on Security and Privacy | May 2006
  
  PDF
- The SMART way to migrate replicated stateful services
  
  Jacob R. Lorch, Atul Adya, William J. Bolosky, Ronnie Chaiken, John R. Douceur, Jon Howell, John (JD) Douceur, Jacob R Lorch, Bill Bolosky
  
  Proceedings of the 2006 EuroSys Conference | April 2006
  
  PDF
- Using user interface event information in dynamic voltage scaling algorithms
  
  Jacob R. Lorch, Alan Jay Smith, Jacob R Lorch
  
  Proceedings of the 11th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS) | October 2003
  
  Proceedings of the 11th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS)
  
  PDF
- Operating system modifications for task-based speed and voltage scheduling
  
  Jacob R Lorch, Alan Jay Smith
  
  Proceedings of the First International Conference on Mobile Systems, Applications, and Services (MobiSys) | May 2003
  
  PDF
- FARSITE: Federated, available, and reliable storage for an incompletely trusted environment
  
  Atul Adya, Bill Bolosky, Miguel Castro, Ronnie Chaiken, Gerald Cermak, John (JD) Douceur, Jon Howell, Jacob R Lorch, Marvin Theimer, Roger Wattenhofer,
  
  Proceedings of the 5th Symposium on Operating Systems Design and Implementation (OSDI) | December 2002
  
  Proceedings of the 5th Symposium on Operating Systems Design and Implementation (OSDI)
  
  PDF
- Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set
  
  Nongyu Di, Tianyu Chen, Shan Lu, Shuai Lu, Yeyun Gong, Peng Cheng, Jacob R Lorch, Yuan Yao, Xiaoxing Ma
  
  February 2026
  
  February 2026
  
  Publication Project
- VeruSAGE: A Study of Agent-Based Verification for Rust Systems
  
  Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jacob R Lorch, Shan Lu
  
  December 2025
  
  December 2025
  
  Preprint Github Project
- The VTrace tool: building a system tracer for Windows NT and Windows 2000
  
  Jacob R. Lorch, Alan Jay Smith, Jacob R Lorch
  
  MSDN Magazine | October 2000, Vol 15(10): pp. 86-102
  
  Publication
- Energy consumption of Apple Macintosh computers
  
  Jacob R. Lorch, Alan Jay Smith, Jacob R Lorch
  
  IEEE Micro | November 1998, Vol 18: pp. 54-63
  
  PDF
- Software Strategies for Portable Computer Energy Management
  
  Jacob R Lorch, Alan Jay Smith
  
  IEEE Personal Communications Magazine | June 1998, pp. 60-73
  
  PDF
- Scheduling techniques for reducing processor energy use in MacOS
  
  Jacob R Lorch, Alan Jay Smith
  
  Wireless Networks | October 1997, pp. 311-324
  
  PDF
- IronFleet: Proving Safety and Liveness of Practical Distributed Systems
  
  Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Justine Stephenson, Srinath Setty, Brian Zill
  
  Communications of the ACM | July 2017, Vol 60
  
  CACM Research Highlight
  
  Publication Project
- PACE: A new approach to dynamic voltage scaling
  
  Jacob R. Lorch, Alan Jay Smith, Jacob R Lorch
  
  IEEE Transactions on Computers | July 2004, Vol 53: pp. 856-869
  
  PDF
- Seamless Customer Identification
  
  Christopher Smowton, Jacob R Lorch, David Molnar, Stefan Saroiu, Alec Wolman
  
  MSR-TR-2013-31 | March 2013
  
  PDF Project
- GreenUp: A Decentralized System for Making Sleeping Machines Available
  
  Siddhartha Sen, Jacob R Lorch, Richard Hughes, Carlos Garcia, Brian Zill, Weverton Cordeiro, Jitu Padhye
  
  MSR-TR-2012-21 | March 2012
  
  PDF
- Memoir—Formal Specs and Correctness Proofs
  
  John (JD) Douceur, Jacob R Lorch, Bryan Parno, James Mickens, Jonathan M. McCune
  
  MSR-TR-2011-19 | February 2011
  
  PDF PDF
- Enabling Security in Cloud Storage SLAs with CloudProof
  
  David Molnar, Jacob R Lorch, Helen Wang, Raluca Ada Popa, Li Zhuang
  
  MSR-TR-2010-46 | May 2010
  
  PDF
- SAV-V: Securing Anti-Virus with Virtualization
  
  Jacob R Lorch, Bryan Parno, Helen Wang
  
  MSR-TR-2011-101 | April 2007
  
  PDF
- Load Management in a Large-Scale Decentralized File System
  
  Atul Adya, Bill Bolosky, Ronnie Chaiken, John (JD) Douceur, Jon Howell, Jacob R Lorch
  
  MSR-TR-2004-60 | July 2004
  
  PDF
- Correctness of Paxos with Replica-Set-Specific Views
  
  Jon Howell, Jacob R Lorch, John (JD) Douceur
  
  MSR-TR-2004-45 | June 2004
  
  PDF PDF
- Operating systems techniques for reducing processor energy consumption
  
  Jacob R Lorch
  
  December 2001
  
  December 2001
  
  PDF

Jay Lorch

Publications

VeruSAGE-Bench: A Benchmark Suite for Rust System Verification

From Lab to Fleet: Building and Deploying a Practical Rowhammer Defense in Cloud SoCs

Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set

VeruSAGE: A Study of Agent-Based Verification for Rust Systems

AutoVerus: Automated Proof Generation for Rust Code

PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection

Verus: A Practical Foundation for Systems Verification

Armada: Low-Effort Verification of High-Performance Concurrent Programs

Capturing and Enhancing In Situ System Observability for Failure Detection

Vale: Verifying High-Performance Cryptographic Assembly Code

IronFleet: Proving Safety and Liveness of Practical Distributed Systems

Gray Failure: The Achilles’ Heel of Cloud-Scale Systems

Everest: Towards a Verified, Drop-In Replacement of HTTPS

Realizing the fault-tolerance promise of cloud storage using locks with intent

IronFleet: Proving Practical Distributed Systems Correct

Tardigrade: Leveraging Lightweight Virtual Machines to Easily and Efficiently Construct Fault-Tolerant Services

Ironclad Apps: End-to-End Security via Automated Full-System Verification

Zero-Effort Payments: Design, Deployment, and Lessons

Composing OS extensions safely and efficiently with Bascule

Seamless Customer Identification

Shroud: Enabling Private Access to Large-Scale Data in the Data Center

Don’t Lose Sleep Over Availability: The GreenUp Decentralized Wakeup Service

GreenUp: A Decentralized System for Making Sleeping Machines Available

Enabling Security in Cloud Storage SLAs with CloudProof

Memoir: Practical State Continuity for Protected Modules

Memoir—Formal Specs and Correctness Proofs

The Utility Coprocessor: Massively Parallel Computation from the Coffee Shop

Enabling Security in Cloud Storage SLAs with CloudProof

Crom: Faster Web Browsing Using Speculative Execution

Matchmaking for online games and other latency-sensitive P2P systems

TrInc: Small Trusted Hardware for Large Distributed Systems

Leveraging legacy code to deploy desktop applications on the Web

Donnybrook: Enabling Large-Scale, High-Speed, Peer-to-Peer Games

A five-year study of file-system metadata

Enhancing game-server AI with distributed client computation

Maximizing Total Upload in Latency-Sensitive P2P Applications

SAV-V: Securing Anti-Virus with Virtualization

Scaling peer-to-peer games in low-bandwidth environments

SubVirt: Implementing malware with virtual machines

The SMART way to migrate replicated stateful services

Load Management in a Large-Scale Decentralized File System

PACE: A new approach to dynamic voltage scaling

Correctness of Paxos with Replica-Set-Specific Views

Using user interface event information in dynamic voltage scaling algorithms

Operating system modifications for task-based speed and voltage scheduling

FARSITE: Federated, available, and reliable storage for an incompletely trusted environment

Improving dynamic voltage scaling algorithms with PACE

Operating systems techniques for reducing processor energy consumption

The VTrace tool: building a system tracer for Windows NT and Windows 2000

A comparison of file system workloads

Energy consumption of Apple Macintosh computers

Software Strategies for Portable Computer Energy Management

Scheduling techniques for reducing processor energy use in MacOS

Reducing Processor Power Consumption by Improving Processor Time Management in a Single-User Operating System

Making World Wide Web caching servers cooperate

VeruSAGE-Bench: A Benchmark Suite for Rust System Verification

Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set

VeruSAGE: A Study of Agent-Based Verification for Rust Systems

AutoVerus: Automated Proof Generation for Rust Code

Seamless Customer Identification

Improving dynamic voltage scaling algorithms with PACE

A comparison of file system workloads

Energy consumption of Apple Macintosh computers

Software Strategies for Portable Computer Energy Management

Scheduling techniques for reducing processor energy use in MacOS

Reducing Processor Power Consumption by Improving Processor Time Management in a Single-User Operating System

Making World Wide Web caching servers cooperate

VeruSAGE-Bench: A Benchmark Suite for Rust System Verification

From Lab to Fleet: Building and Deploying a Practical Rowhammer Defense in Cloud SoCs

Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set

VeruSAGE: A Study of Agent-Based Verification for Rust Systems

AutoVerus: Automated Proof Generation for Rust Code

PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection

Verus: A Practical Foundation for Systems Verification

Armada: Low-Effort Verification of High-Performance Concurrent Programs

Capturing and Enhancing In Situ System Observability for Failure Detection

IronFleet: Proving Safety and Liveness of Practical Distributed Systems

Gray Failure: The Achilles’ Heel of Cloud-Scale Systems