Generating Tests from Counterexamples. - Dirk Beyer 001; Adam Chlipala; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (ICSE, 2004)

Invited talk: the blast query language for software verification. - Dirk Beyer 001; Adam Chlipala; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (PEPM, 2004)

The Blast Query Language for Software Verification.. - Dirk Beyer 001; Adam Chlipala; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (SAS, 2004)

The open verifier framework for foundational verifiers. - Bor-Yuh Evan Chang; Adam Chlipala; George C. Necula; Robert R. Schneck (TLDI, 2005)

Type-based verification of assembly language for compiler debugging. - Bor-Yuh Evan Chang; Adam Chlipala; George C. Necula; Robert R. Schneck (TLDI, 2005)

Strict bidirectional type checking. - Adam Chlipala; Leaf Petersen; Robert Harper 001 (TLDI, 2005)

A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. - Bor-Yuh Evan Chang; Adam Chlipala; George C. Necula (VMCAI, 2006)

Position Paper: Thoughts on Programming with Proof Assistants. - Adam Chlipala (PLPV@IJCAR, 2006)

A certified type-preserving compiler from lambda calculus to assembly language. - Adam Chlipala (PLDI, 2007)

Parametric higher-order abstract syntax for mechanized semantics. - Adam Chlipala (ICFP, 2008)

Modular development of certified program verifiers with a proof assistant, . - Adam Chlipala (J. Funct. Program., 2008)

Effective interactive proofs for higher-order imperative programs. - Adam Chlipala; J. Gregory Malecha; Greg Morrisett; Avraham Shinnar; Ryan Wisnesky (ICFP, 2009)

Foundational Program Verification in Coq with Automated Proofs. - Adam Chlipala (MSFP@ICFP, 2010)

Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications. - Adam Chlipala (OSDI, 2010)

Ur: statically-typed metaprogramming with type-level record computation. - Adam Chlipala (PLDI, 2010)

A verified compiler for an impure functional language. - Adam Chlipala (POPL, 2010)

An Introduction to Programming and Proving with Dependent Types in Coq. - Adam Chlipala (J. Formaliz. Reason., 2010)

Mostly-automated verification of low-level programs in computational separation logic. - Adam Chlipala (PLDI, 2011)

Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. - Adam Chlipala (MIT Press, 2013)

Formal Verification of Hardware Synthesis. - Thomas Braibant; Adam Chlipala (CAV, 2013)

The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. - Adam Chlipala (ICFP, 2013)

MirrorShard: Proof by Computational Reflection with Verified Hints - Gregory Malecha; Adam Chlipala; Thomas Braibant; Patrick Hulin; Edward Z. Yang (CoRR, 2013)

Experience Implementing a Performant Category-Theory Library in Coq. - Jason Gross; Adam Chlipala; David I. Spivak (ITP, 2014)

Compositional Computational Reflection. - Gregory Malecha; Adam Chlipala; Thomas Braibant (ITP, 2014)

Compiler verification meets cross-language linking via data abstraction. - Peng Wang 048; Santiago Cuéllar; Adam Chlipala (OOPSLA, 2014)

Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. - Xi Wang 005; David Lazar; Nickolai Zeldovich; Adam Chlipala; Zachary Tatlock (OSDI, 2014)

Modular Deductive Verification of Multiprocessor Hardware Designs. - Muralidaran Vijayaraghavan; Adam Chlipala; Arvind 001; Nirav Dave (CAV (2), 2015)

Specifying Crash Safety for Storage Systems. - Haogang Chen 001; Daniel Ziegler 002; Adam Chlipala; M. Frans Kaashoek; Eddie Kohler; Nickolai Zeldovich (HotOS, 2015)

An optimizing compiler for a purely functional web-application language. - Adam Chlipala (ICFP, 2015)

From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification. - Adam Chlipala (POPL, 2015)

Proof engineering: implementation challenges in rigorously verified software. - Adam Chlipala (PLMW@POPL, 2015)

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. - Benjamin Delaware; Clément Pit-Claudel; Jason Gross; Adam Chlipala (POPL, 2015)

Chapar: certified causally consistent distributed key-value stores. - Mohsen Lesani; Christian J. Bell; Adam Chlipala (POPL, 2016)

Using Crash Hoare Logic for Certifying the FSCQ File System. - Haogang Chen 001; Daniel Ziegler 002; Tej Chajed; Adam Chlipala; M. Frans Kaashoek; Nickolai Zeldovich (USENIX ATC, 2016)

Ur/Web: a simple model for programming the web. - Adam Chlipala (Commun. ACM, 2016)

A program optimization for automatic database result caching. - Ziv Scully; Adam Chlipala (POPL, 2017)

The End of History? Using a Proof Assistant to Replace Language Design with Library Design. - Adam Chlipala; Benjamin Delaware; Samuel Duchovni; Jason Gross; Clément Pit-Claudel; Sorawit Suriyakarn; Peng Wang 048; Katherine Ye (SNAPL, 2017)

Verifying a high-performance crash-safe file system using a tree specification. - Haogang Chen 001; Tej Chajed; Alex Konradi; Stephanie Wang; Atalay Mert Ileri; Adam Chlipala; M. Frans Kaashoek; Nickolai Zeldovich (SOSP, 2017)

Certifying a file system using crash hoare logic: correctness in the presence of crashes. - Tej Chajed; Haogang Chen 001; Adam Chlipala; M. Frans Kaashoek; Nickolai Zeldovich; Daniel Ziegler 002 (Commun. ACM, 2017)

Kami: a platform for high-level parametric hardware specification and its modular verification. - Joonwon Choi; Muralidaran Vijayaraghavan; Benjamin Sherman; Adam Chlipala; Arvind 001 (Proc. ACM Program. Lang., 2017)

TiML: a functional language for practical complexity analysis with invariants. - Peng Wang 048; Di Wang 017; Adam Chlipala (Proc. ACM Program. Lang., 2017)

Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac. - Jason Gross; Andres Erbsen; Adam Chlipala (ITP, 2018)

Computable decision making on the reals and other spaces: via partiality and nondeterminism. - Benjamin Sherman; Luke Sciarappa; Adam Chlipala; Michael Carbin (LICS, 2018)

Proving confidentiality in a file system using DiskSec. - Atalay Mert Ileri; Tej Chajed; Adam Chlipala; M. Frans Kaashoek; Nickolai Zeldovich (OSDI, 2018)

Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats. - Sorawit Suriyakarn; Clément Pit-Claudel; Benjamin Delaware; Adam Chlipala (CoRR, 2018)

Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam. - Antonis Stampoulis; Adam Chlipala (Proc. ACM Program. Lang., 2018)

Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. - Thomas Grégoire; Adam Chlipala (J. Autom. Reason., 2019)

Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. - Benjamin Delaware; Sorawit Suriyakarn; Clément Pit-Claudel; Qianchuan Ye; Adam Chlipala (Proc. ACM Program. Lang., 2019)

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. - Clément Pit-Claudel; Peng Wang 048; Benjamin Delaware; Jason Gross; Adam Chlipala (IJCAR (2), 2020)

Proof assistants at the hardware-software interface (invited talk). - Adam Chlipala (CPP, 2020)

The essence of Bluespec: a core language for rule-based hardware design. - Thomas Bourgeat; Clément Pit-Claudel; Adam Chlipala; Arvind 001 (PLDI, 2020)

Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises. - Andres Erbsen; Jade Philipoom; Jason Gross; Robert Sloan 001; Adam Chlipala (ACM SIGOPS Oper. Syst. Rev., 2020)

Effective simulation and debugging for a high-level hardware language using software compilers. - Clément Pit-Claudel; Thomas Bourgeat; Stella Lau; Arvind 001; Adam Chlipala (ASPLOS, 2021)

Integration verification across software and hardware for a simple embedded system. - Andres Erbsen; Samuel Gruetter; Joonwon Choi; Clark Wood; Adam Chlipala (PLDI, 2021)

A Multipurpose Formal RISC-V Specification. - Thomas Bourgeat; Ian Clester; Andres Erbsen; Samuel Gruetter; Andrew Wright; Adam Chlipala (CoRR, 2021)

Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl). - Adam Chlipala (Proc. ACM Program. Lang., 2021)

Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols. - Joonwon Choi; Adam Chlipala; Arvind 001 (CAV (2), 2022)

Adversary Safety by Construction in a Language of Cryptographic Protocols. - Timothy M. Braje; Alice R. Lee; Andrew Wagner; Benjamin Kaiser; Daniel Park; Martine Kalke; Robert K. Cunningham; Adam Chlipala (CSF, 2022)

Accelerating Verified-Compiler Development with a Verified Rewriting Engine. - Jason Gross; Andres Erbsen; Jade Philipoom; Miraya Poddar-Agrawal; Adam Chlipala (ITP, 2022)

Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. - Jason Gross; Théo Zimmermann; Miraya Poddar-Agrawal; Adam Chlipala (ITP, 2022)

Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. - Clément Pit-Claudel; Jade Philipoom; Dustin Jamner; Andres Erbsen; Adam Chlipala (PLDI, 2022)

CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives. - Joel Kuepper; Andres Erbsen; Jason Gross; Owen Conoly; Chuyue Sun; Samuel Tian; David Wu; Adam Chlipala; Chitchanok Chuengsatiansup; Daniel Genkin; Markus Wagner 007; Yuval Yarom (CoRR, 2022)

Certifying derivation of state machines from coroutines. - Mirai Ikebuchi; Andres Erbsen; Adam Chlipala (Proc. ACM Program. Lang., 2022)

C4: verified transactional objects. - Mohsen Lesani; Li-yao Xia; Anders Kaseorg; Christian J. Bell; Adam Chlipala; Benjamin C. Pierce; Steve Zdancewic (Proc. ACM Program. Lang., 2022)

Verified tensor-program optimization via high-level scheduling rewrites. - Amanda Liu; Gilbert Louis Bernstein; Adam Chlipala; Jonathan Ragan-Kelley (Proc. ACM Program. Lang., 2022)

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 007; Yuval Yarom (ICSE Companion, 2023)

CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives. - Joel Kuepper; Andres Erbsen; Jason Gross; Owen Conoly; Chuyue Sun; Samuel Tian; David Wu; Adam Chlipala; Chitchanok Chuengsatiansup; Daniel Genkin; Markus Wagner 007; Yuval Yarom (Proc. ACM Program. Lang., 2023)

Omnisemantics: Smooth Handling of Nondeterminism. - Arthur Charguéraud; Adam Chlipala; Andres Erbsen; Samuel Gruetter (ACM Trans. Program. Lang. Syst., 2023)

Flexible Instruction-Set Semantics via Abstract Monads (Experience Report). - Thomas Bourgeat; Ian Clester; Andres Erbsen; Samuel Gruetter; Pratap Singh; Andy Wright; Adam Chlipala (Proc. ACM Program. Lang., 2023)

Specification and Verification of Strong Timing Isolation of Hardware Enclaves. - Stella Lau; Thomas Bourgeat; Clément Pit-Claudel; Adam Chlipala (CCS, 2024)

Probability from Possibility: Probabilistic Confidentiality for Storage Systems Under Nondeterminism. - Atalay Mert Ileri; Nickolai Zeldovich; Adam Chlipala; M. Frans Kaashoek (CSF, 2024)

Verifying Software Emulation of an Unsupported Hardware Instruction. - Samuel Gruetter; Thomas Bourgeat; Adam Chlipala (ITP, 2024)

Foundational Integration Verification of a Cryptographic Server. - Andres Erbsen; Jade Philipoom; Dustin Jamner; Ashley Lin; Samuel Gruetter; Clément Pit-Claudel; Adam Chlipala (Proc. ACM Program. Lang., 2024)

Live Verification in an Interactive Proof Assistant. - Samuel Gruetter; Viktor Fukala; Adam Chlipala (Proc. ACM Program. Lang., 2024)

A Verified Compiler for a Functional Tensor Language. - Amanda Liu; Gilbert Bernstein; Adam Chlipala; Jonathan Ragan-Kelley (Proc. ACM Program. Lang., 2024)

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq. - Jason Gross; Andres Erbsen; Jade Philipoom; Rajashree Agrawal; Adam Chlipala (J. Autom. Reason., 2024)

Making Concurrent Hardware Verification Sequential. - Thomas Bourgeat; Jiazheng Liu; Adam Chlipala; Arvind 001 (PLDI, 2025)

Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers. - Owen Conoly; Andres Erbsen; Adam Chlipala (Proc. ACM Program. Lang., 2025)

PLanet: Formalizing Experimental Design. - London Bielicke; Anna Zhang; Shruti Tyagi; Emery D. Berger; Adam Chlipala; Eunice Jun (CoRR, 2025)

Pyrosome: Verified Compilation for Modular Metatheory. - Dustin Jamner; Gabriel Kammer; Ritam Nag; Adam Chlipala (CoRR, 2025)