PLDI 2026 (series) / PLDI Research Papers /
[TOPLAS] Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software
Danel Ahman, Karthikeyan Bhargavan, Barry Bond, Jay Bosamiya, Christopher Brzuska, Antoine Delignat-Lavaud, Cédric Fournet, Aymeric Fromherz, Sydney Gibson, Chris Hawblitzel, Cătălin Hriţcu, Markulf Kohlweiss, Guido Martínez, Haobin Ni, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Exequiel Rivas, Nikhil Swamy, Santiago Zanella-Béguelin
This program is tentative and subject to change.
Fri 19 Jun 2026 15:00 - 15:20 at Flatirons 2 - Verification and Proof Reasoning
Project Everest began at Microsoft Research in 2016, aiming to spur research in program verification to produce industrial-grade software. In collaboration with INRIA and Carnegie Mellon University, Project Everest’s goal was to produce drop-in verified replacements of secure communications software used in the HTTPS ecosystem, including TLS, the underlying cryptography, and related subprotocols. Now, almost a decade later, we reflect on the project, sharing both its successes and failures, and look ahead to the next decade of program verification research.
This program is tentative and subject to change.
Fri 19 JunDisplayed time zone: Mountain Time (US & Canada) change
Fri 19 Jun
Displayed time zone: Mountain Time (US & Canada) change
13:40 - 15:20 | |||
13:40 20mTalk | Heterogeneous Dynamic Logic: Provability Modulo Program Theories PLDI Research Papers DOI | ||
14:00 20mTalk | Intrinsically Correct Algorithms and Recursive Coalgebras PLDI Research Papers Cass Alexandru RPTU Kaiserslautern-Landau, Henning Urbat Friedrich-Alexander University Erlangen-Nürnberg, Thorsten Wißmann Friedrich-Alexander University Erlangen-Nürnberg DOI | ||
14:20 20mTalk | CRIS: The Power of Imagination in Hybrid Verification PLDI Research Papers Yonghee Kim Seoul National University, Taeyoung Yoon Seoul National University, Sanghyun Yi Seoul National University, Jaehyung Lee Seoul National University, Soonwon Moon Seoul National University, Yeji Han Seoul National University, Seonho Lee Seoul National University, Taeyoung Rhee Seoul National University, Yujin Im Seoul National University, Donghyun Nam Seoul National University, Jieung Kim Yonsei University, Chung-Kil Hur Seoul National University DOI | ||
14:40 20mTalk | Navigating AND–OR Graph Modifications to Debug Failing Proof Search PLDI Research Papers Justin Lubin University of California at Berkeley, Marlena Preigh University of California at Berkeley, Max Willsey University of California at Berkeley, Sarah E. Chasins University of California at Berkeley DOI | ||
15:00 20mTalk | [TOPLAS] Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software PLDI Research Papers Danel Ahman University of Ljubljana, Karthikeyan Bhargavan Cryspen, France, Barry Bond , Jay Bosamiya Microsoft Research, Christopher Brzuska , Antoine Delignat-Lavaud Microsoft Research, n.n., Cédric Fournet Microsoft Research, Aymeric Fromherz Inria, Sydney Gibson , Chris Hawblitzel Microsoft Research, Cătălin Hriţcu MPI-SP, Markulf Kohlweiss , Guido Martínez Microsoft Research, Haobin Ni University of Washington, Bryan Parno Carnegie Mellon University, Jonathan Protzenko Microsoft Azure Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Exequiel Rivas Tallinn University of Technology, Nikhil Swamy Microsoft Research, Santiago Zanella-Béguelin Microsoft Research, Cambridge | ||