| 2026 | CHI | On the Common Pitfalls of Designing and Communicating Within-Subjects Experiments in HCI. | London Bielicke, Emery D. Berger, Adam Chlipala, Eunice Jun |
| 2026 | CPP | Foundational Verification of Running-Time Bounds for Interactive Programs. | Andy Tockman, Pratap Singh, Andres Erbsen, Samuel Gruetter, Adam Chlipala |
| 2025 | CCS | Securing Cryptographic Software via Typed Assembly Language. | Shixin Song, Tingzhen Dong, Kosi Nwabueze, Julian Zanders, Andres Erbsen, Adam Chlipala, Mengjia Yan |
| 2024 | CCS | Specification and Verification of Strong Timing Isolation of Hardware Enclaves. | Stella Lau, Thomas Bourgeat, Clment Pit-Claudel, Adam Chlipala |
| 2024 | ITP | Verifying Software Emulation of an Unsupported Hardware Instruction. | Samuel Gruetter, Thomas Bourgeat, Adam Chlipala |
| 2023 | ICSE | CryptOpt: Automatic Optimization of Straightline Code. | Joel Kuepper, David Wu, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom |
| 2022 | CAV | Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols. | Joonwon Choi, Adam Chlipala, Arvind |
| 2022 | ITP | Accelerating Verified-Compiler Development with a Verified Rewriting Engine. | Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala |
| 2022 | ITP | Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. | Jason Gross, Tho Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala |
| 2022 | PLDI | Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. | Clment Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala |
| 2021 | ASPLOS | Effective simulation and debugging for a high-level hardware language using software compilers. | Clment Pit-Claudel, Thomas Bourgeat, Stella Lau, Arvind, Adam Chlipala |
| 2021 | PLDI | Integration verification across software and hardware for a simple embedded system. | Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, Adam Chlipala |
| 2020 | CADE | Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. | Clment Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala |
| 2020 | CPP | Proof assistants at the hardware-software interface (invited talk). | Adam Chlipala |
| 2020 | PLDI | The essence of Bluespec: a core language for rule-based hardware design. | Thomas Bourgeat, Clment Pit-Claudel, Adam Chlipala, Arvind |
| 2019 | SP | Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises. | Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala |
| 2018 | ITP | Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac. | Jason Gross, Andres Erbsen, Adam Chlipala |
| 2018 | LICS | Computable decision making on the reals and other spaces: via partiality and nondeterminism. | Benjamin Sherman, Luke Sciarappa, Adam Chlipala, Michael Carbin |
| 2018 | OSDI | Proving confidentiality in a file system using DiskSec. | Atalay Mert Ileri, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich |
| 2017 | POPL | A program optimization for automatic database result caching. | Ziv Scully, Adam Chlipala |
| 2017 | SOSP | Verifying a high-performance crash-safe file system using a tree specification. | Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay Mert Ileri, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich |
| 2016 | ITP | Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. | Thomas Grgoire, Adam Chlipala |
| 2016 | POPL | Chapar: certified causally consistent distributed key-value stores. | Mohsen Lesani, Christian J. Bell, Adam Chlipala |
| 2016 | USENIX | Using Crash Hoare Logic for Certifying the FSCQ File System. | Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich |
| 2015 | CAV | Modular Deductive Verification of Multiprocessor Hardware Designs. | Muralidaran Vijayaraghavan, Adam Chlipala, Arvind, Nirav Dave |
| 2015 | HotOS | Specifying Crash Safety for Storage Systems. | Haogang Chen, Daniel Ziegler, Adam Chlipala, M. Frans Kaashoek, Eddie Kohler, Nickolai Zeldovich |
| 2015 | ICFP | An optimizing compiler for a purely functional web-application language. | Adam Chlipala |
| 2015 | POPL | Ur/Web: A Simple Model for Programming the Web. | Adam Chlipala |
| 2015 | POPL | From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification. | Adam Chlipala |
| 2015 | POPL | Proof engineering: implementation challenges in rigorously verified software. | Adam Chlipala |
| 2015 | POPL | Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. | Benjamin Delaware, Clment Pit-Claudel, Jason Gross, Adam Chlipala |
| 2015 | SOSP | Using Crash Hoare logic for certifying the FSCQ file system. | Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich |
| 2014 | ITP | Experience Implementing a Performant Category-Theory Library in Coq. | Jason Gross, Adam Chlipala, David I. Spivak |
| 2014 | ITP | Compositional Computational Reflection. | Gregory Malecha, Adam Chlipala, Thomas Braibant |
| 2014 | OOPSLA | Compiler verification meets cross-language linking via data abstraction. | Peng Wang, Santiago Cullar, Adam Chlipala |
| 2014 | OSDI | Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. | Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock |
| 2013 | CAV | Formal Verification of Hardware Synthesis. | Thomas Braibant, Adam Chlipala |
| 2013 | ICFP | The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. | Adam Chlipala |
| 2011 | PLDI | Mostly-automated verification of low-level programs in computational separation logic. | Adam Chlipala |
| 2010 | ICFP | Foundational Program Verification in Coq with Automated Proofs. | Adam Chlipala |
| 2010 | OSDI | Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications. | Adam Chlipala |
| 2010 | PLDI | Ur: statically-typed metaprogramming with type-level record computation. | Adam Chlipala |
| 2010 | POPL | A verified compiler for an impure functional language. | Adam Chlipala |
| 2009 | ICFP | Effective interactive proofs for higher-order imperative programs. | Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky |
| 2008 | ICFP | Parametric higher-order abstract syntax for mechanized semantics. | Adam Chlipala |
| 2007 | PLDI | A certified type-preserving compiler from lambda calculus to assembly language. | Adam Chlipala |
| 2006 | ICFP | Modular development of certified program verifiers with a proof assistant. | Adam Chlipala |
| 2006 | VMCAI | A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. | Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula |
| 2004 | ICSE | Generating Tests from Counterexamples. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | PEPM | Invited talk: the blast query language for software verification. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | PPDP | Invited talk: the blast query language for software verification. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | SAS | The Blast Query Language for Software Verification.. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |