Adam Chlipala

Publication Activity (10 Years)

Years Active: 2004-2024
Publications (10 Years): 48

Top Topics

Formal Verification

Functional Language

Hardware Design

Top Venues

Proc. ACM Program. Lang.

Publications

Samuel Gruetter, Viktor Fukala, Adam Chlipala
Live Verification in an Interactive Proof Assistant. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Amanda Liu, Gilbert Bernstein, Adam Chlipala, Jonathan Ragan-Kelley
A Verified Compiler for a Functional Tensor Language. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq. J. Autom. Reason. 68 (3) (2024)
Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel, Adam Chlipala
Foundational Integration Verification of a Cryptographic Server. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Joel Kuepper, David Wu, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
CryptOpt: Automatic Optimization of Straightline Code. ICSE Companion (2023)
Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter
Omnisemantics: Smooth Handling of Nondeterminism. ACM Trans. Program. Lang. Syst. 45 (1) (2023)
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
CryptOpt: Automatic Optimization of Straightline Code. CoRR (2023)
Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andy Wright, Adam Chlipala
Flexible Instruction-Set Semantics via Abstract Monads (Experience Report). Proc. ACM Program. Lang. 7 (ICFP) (2023)
Jason Gross, Andres Erbsen, Jade Philipoom, Rajashree Agrawal, Adam Chlipala
Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq. CoRR (2023)
Mirai Ikebuchi, Andres Erbsen, Adam Chlipala
Certifying derivation of state machines from coroutines. Proc. ACM Program. Lang. 6 (POPL) (2022)
Timothy M. Braje, Alice R. Lee, Andrew Wagner, Benjamin Kaiser, Daniel Park, Martine Kalke, Robert K. Cunningham, Adam Chlipala
Adversary Safety by Construction in a Language of Cryptographic Protocols. CSF (2022)
Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala
Accelerating Verified-Compiler Development with a Verified Rewriting Engine. CoRR (2022)
Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, Jonathan Ragan-Kelley
Verified tensor-program optimization via high-level scheduling rewrites. Proc. ACM Program. Lang. 6 (POPL) (2022)
Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, Steve Zdancewic
C4: verified transactional objects. Proc. ACM Program. Lang. 6 (OOPSLA) (2022)
Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun, Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel Genkin, Markus Wagner, Yuval Yarom
CryptOpt: Verified Compilation with Random Program Search for Cryptographic Primitives. CoRR (2022)
Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala
Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. PLDI (2022)
Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala
Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. ITP (2022)
Jason Gross, Andres Erbsen, Jade Philipoom, Miraya Poddar-Agrawal, Adam Chlipala
Accelerating Verified-Compiler Development with a Verified Rewriting Engine. ITP (2022)
Joonwon Choi, Adam Chlipala, Arvind
Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols. CAV (2) (2022)
Jason Gross, Théo Zimmermann, Miraya Poddar-Agrawal, Adam Chlipala
Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq. CoRR (2022)
Adam Chlipala
Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl). Proc. ACM Program. Lang. 5 (ICFP) (2021)
Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Andrew Wright, Adam Chlipala
A Multipurpose Formal RISC-V Specification. CoRR (2021)
Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, Adam Chlipala
Integration verification across software and hardware for a simple embedded system. PLDI (2021)
Clément Pit-Claudel, Thomas Bourgeat, Stella Lau, Arvind, Adam Chlipala
Effective simulation and debugging for a high-level hardware language using software compilers. ASPLOS (2021)
Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs. IJCAR (2) (2020)
Adam Chlipala
Proof assistants at the hardware-software interface (invited talk). CPP (2020)
Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, Arvind
The essence of Bluespec: a core language for rule-based hardware design. PLDI (2020)
Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala
Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises. ACM SIGOPS Oper. Syst. Rev. 54 (1) (2020)
Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala
Narcissus: correct-by-construction derivation of decoders and encoders from binary formats. Proc. ACM Program. Lang. 3 (ICFP) (2019)
Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala
Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises. IEEE Symposium on Security and Privacy (2019)
Thomas Grégoire, Adam Chlipala
Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. J. Autom. Reason. 62 (2) (2019)
Atalay Mert Ileri, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich
Proving confidentiality in a file system using DiskSec. OSDI (2018)
Benjamin Sherman, Luke Sciarappa, Adam Chlipala, Michael Carbin
Computable decision making on the reals and other spaces: via partiality and nondeterminism. LICS (2018)
Benjamin Sherman, Luke Sciarappa, Adam Chlipala, Michael Carbin
Computable decision making on the reals and other spaces via partiality and nondeterminism. CoRR (2018)
Sorawit Suriyakarn, Clément Pit-Claudel, Benjamin Delaware, Adam Chlipala
Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats. CoRR (2018)
Antonis Stampoulis, Adam Chlipala
Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Jason Gross, Andres Erbsen, Adam Chlipala
Reification by Parametricity - Fast Setup for Proof by Reflection, in Two Lines of Ltac. ITP (2018)
Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye
The End of History? Using a Proof Assistant to Replace Language Design with Library Design. SNAPL (2017)
Tej Chajed, Haogang Chen, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich, Daniel Ziegler
Certifying a file system using crash hoare logic: correctness in the presence of crashes. Commun. ACM 60 (4) (2017)
Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, Arvind
Kami: a platform for high-level parametric hardware specification and its modular verification. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay Mert Ileri, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich
Verifying a high-performance crash-safe file system using a tree specification. SOSP (2017)
Ziv Scully, Adam Chlipala
A program optimization for automatic database result caching. POPL (2017)
Peng Wang, Di Wang, Adam Chlipala
TiML: a functional language for practical complexity analysis with invariants. Proc. ACM Program. Lang. 1 (OOPSLA) (2017)
Adam Chlipala
Ur/Web: a simple model for programming the web. Commun. ACM 59 (8) (2016)
Mohsen Lesani, Christian J. Bell, Adam Chlipala
Chapar: certified causally consistent distributed key-value stores. POPL (2016)
Thomas Grégoire, Adam Chlipala
Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. ITP (2016)
Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich
Using Crash Hoare Logic for Certifying the FSCQ File System. USENIX Annual Technical Conference (2016)
Muralidaran Vijayaraghavan, Adam Chlipala, Arvind, Nirav Dave
Modular Deductive Verification of Multiprocessor Hardware Designs. CAV (2) (2015)
Adam Chlipala
Proof engineering: implementation challenges in rigorously verified software. PLMW@POPL (2015)
Adam Chlipala
Ur/Web: A Simple Model for Programming the Web. POPL (2015)
Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich
Using Crash Hoare logic for certifying the FSCQ file system. SOSP (2015)
Adam Chlipala
From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification. POPL (2015)
Benjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. POPL (2015)
Adam Chlipala
An optimizing compiler for a purely functional web-application language. ICFP (2015)
Haogang Chen, Daniel Ziegler, Adam Chlipala, M. Frans Kaashoek, Eddie Kohler, Nickolai Zeldovich
Specifying Crash Safety for Storage Systems. HotOS (2015)
Gregory Malecha, Adam Chlipala, Thomas Braibant
Compositional Computational Reflection. ITP (2014)
Jason Gross, Adam Chlipala, David I. Spivak
Experience Implementing a Performant Category-Theory Library in Coq. CoRR (2014)
Xi Wang, David Lazar, Nickolai Zeldovich, Adam Chlipala, Zachary Tatlock
Jitk: A Trustworthy In-Kernel Interpreter Infrastructure. OSDI (2014)
Peng Wang, Santiago Cuellar, Adam Chlipala
Compiler verification meets cross-language linking via data abstraction. OOPSLA (2014)
Jason Gross, Adam Chlipala, David I. Spivak
Experience Implementing a Performant Category-Theory Library in Coq. ITP (2014)
Adam Chlipala
The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. ICFP (2013)
Thomas Braibant, Adam Chlipala
Formal Verification of Hardware Synthesis. CAV (2013)
Thomas Braibant, Adam Chlipala
Formal Verification of Hardware Synthesis CoRR (2013)
Gregory Malecha, Adam Chlipala, Thomas Braibant, Patrick Hulin, Edward Z. Yang
MirrorShard: Proof by Computational Reflection with Verified Hints CoRR (2013)
Adam Chlipala
Mostly-automated verification of low-level programs in computational separation logic. PLDI (2011)
Adam Chlipala
Foundational Program Verification in Coq with Automated Proofs. MSFP@ICFP (2010)
Adam Chlipala
A verified compiler for an impure functional language. POPL (2010)
Adam Chlipala
Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications. OSDI (2010)
Adam Chlipala
Ur: statically-typed metaprogramming with type-level record computation. PLDI (2010)
Adam Chlipala
An Introduction to Programming and Proving with Dependent Types in Coq. J. Formaliz. Reason. 3 (2) (2010)
Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky
Effective interactive proofs for higher-order imperative programs. ICFP (2009)
Adam Chlipala
Parametric higher-order abstract syntax for mechanized semantics. ICFP (2008)
Adam Chlipala
Modular development of certified program verifiers with a proof assistant, . J. Funct. Program. 18 (5-6) (2008)
Adam Chlipala
Position Paper: Thoughts on Programming with Proof Assistants. Electron. Notes Theor. Comput. Sci. 174 (7) (2007)
Adam Chlipala
A certified type-preserving compiler from lambda calculus to assembly language. PLDI (2007)
Adam Chlipala
Modular development of certified program verifiers with a proof assistant. ICFP (2006)
Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula
A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety. VMCAI (2006)
Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck
The open verifier framework for foundational verifiers. TLDI (2005)
Bor-Yuh Evan Chang, Adam Chlipala, George C. Necula, Robert R. Schneck
Type-based verification of assembly language for compiler debugging. TLDI (2005)
Adam Chlipala, Leaf Petersen, Robert Harper
Strict bidirectional type checking. TLDI (2005)
Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
The Blast Query Language for Software Verification.. SAS (2004)
Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
Invited talk: the blast query language for software verification. PPDP (2004)
Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
Invited talk: the blast query language for software verification. PEPM (2004)
Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
Generating Tests from Counterexamples. ICSE (2004)