| 2024 | CPP | VCFloat2: Floating-Point Error Analysis in Coq. | Andrew W. Appel, Ariel Kellison |
| 2023 | ARITH | LAProof: A Library of Formal Proofs of Accuracy and Correctness for Linear Algebra Programs. | Ariel E. Kellison, Andrew W. Appel, Mohit Tekriwal, David Bindel |
| 2023 | ITP | Foundational Verification of Stateful P4 Packet Processing. | Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, Andrew W. Appel |
| 2022 | CAV | Verified Erasure Correction in Coq with MathComp and VST. | Joshua M. Cohen, Qinshi Wang, Andrew W. Appel |
| 2022 | CAV | Verified Numerical Methods for Ordinary Differential Equations. | Ariel E. Kellison, Andrew W. Appel |
| 2022 | CPP | Coq's vibrant ecosystem for verification engineering (invited talk). | Andrew W. Appel |
| 2020 | ESOP | Connecting Higher-Order Separation Logic to a First-Order Outside World. | William Mansky, Wolf Honor, Andrew W. Appel |
| 2019 | FM | Abstraction and Subsumption in Modular Verification of C Programs. | Lennart Beringer, Andrew W. Appel |
| 2017 | APLAS | Bringing Order to the Separation Logic Jungle. | Qinxiang Cao, Santiago Cullar, Andrew W. Appel |
| 2017 | CCS | Verified Correctness and Security of mbedTLS HMAC-DRBG. | Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, Andrew W. Appel |
| 2017 | PPDP | Shrink fast correctly! | Olivier Savary Blanger, Andrew W. Appel |
| 2015 | PLDI | Verification of a cryptographic primitive: SHA-256 (abstract). | Andrew W. Appel |
| 2015 | POPL | Compositional CompCert. | Gordon Stewart, Lennart Beringer, Santiago Cullar, Andrew W. Appel |
| 2014 | ESOP | Verified Compilation for Shared-Memory C. | Lennart Beringer, Gordon Stewart, Robert Dockins, Andrew W. Appel |
| 2013 | CPP | Mostly Sound Type System Improves a Foundational Program Verifier. | Josiah Dodds, Andrew W. Appel |
| 2012 | ICFP | Verified heap theorem prover by paramodulation. | Gordon Stewart, Lennart Beringer, Andrew W. Appel |
| 2011 | CPP | VeriSmall: Verified Smallfoot Shape Analysis. | Andrew W. Appel |
| 2011 | ESOP | Verified Software Toolchain - (Invited Talk). | Andrew W. Appel |
| 2010 | APLAS | A Logical Mix of Approximation and Separation. | Aquinas Hobor, Robert Dockins, Andrew W. Appel |
| 2010 | ESOP | Formal Verification of Coalescing Graph-Coloring Register Allocation. | Sandrine Blazy, Benot Robillard, Andrew W. Appel |
| 2010 | POPL | A theory of indirection via approximation. | Aquinas Hobor, Robert Dockins, Andrew W. Appel |
| 2010 | SAS | Concurrent Separation Logic for Pipelined Parallelization. | Christian J. Bell, Andrew W. Appel, David Walker |
| 2009 | APLAS | A Fresh Look at Separation Algebras and Share Accounting. | Robert Dockins, Aquinas Hobor, Andrew W. Appel |
| 2008 | ESOP | Oracle Semantics for Concurrent Separation Logic. | Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli |
| 2007 | POPL | A very modal model of a modern, major, general type system. | Andrew W. Appel, Paul-Andr Mellis, Christopher D. Richards, Jrme Vouillon |
| 2006 | VMCAI | A Compositional Logic for Control Flow. | Gang Tan, Andrew W. Appel |
| 2004 | PLDI | Social processes and proofs of theorems and programs, revisited. | Andrew W. Appel |
| 2004 | VMCAI | Construction of a Semantic Model for a Typed Assembly Language. | Gang Tan, Andrew W. Appel, Kedar N. Swadi, Dinghao Wu |
| 2003 | PLDI | A provably sound TAL for back-end optimization. | Juan Chen, Dinghao Wu, Andrew W. Appel, Hai Fang |
| 2003 | PPDP | Foundational proof checkers with small witnesses. | Dinghao Wu, Andrew W. Appel, Aaron Stump |
| 2003 | SP | Using Memory Errors to Attack a Virtual Machine. | Sudhakar Govindavajhala, Andrew W. Appel |
| 2002 | LICS | A Stratified Semantics of General References A Stratified Semantics of General References. | Amal J. Ahmed, Andrew W. Appel, Roberto Virga |
| 2002 | OOPSLA | Creating and preserving locality of java applications at allocation and garbage collection times. | Yefim Shuf, Manish Gupta, Hubertus Franke, Andrew W. Appel, Jaswinder Pal Singh |
| 2001 | LICS | Foundational Proof-Carrying Code. | Andrew W. Appel |
| 2001 | PLDI | Optimal Spilling for CISC Machines with Few Registers. | Andrew W. Appel, Lal George |
| 2001 | POPL | Type-preserving garbage collectors. | Daniel C. Wang, Andrew W. Appel |
| 2000 | CADE | Machine Instruction Syntax and Semantics in Higher Order Logic. | Neophytos G. Michael, Andrew W. Appel |
| 2000 | POPL | A Semantic Model of Types and Machine Instructions for Proof-Carrying Code. | Andrew W. Appel, Amy P. Felty |
| 1999 | CCS | Proof-Carrying Authentication. | Andrew W. Appel, Edward W. Felten |
| 1999 | ICLP | Lightweight Lemmas in lambda-Prolog. | Andrew W. Appel, Amy P. Felty |
| 1997 | ICFP | Lambda-Splitting: A Higher-Order Approach to Cross-Module Optimizations. | Matthias Blume, Andrew W. Appel |
| 1996 | POPL | Iterated Register Coalescing. | Lal George, Andrew W. Appel |
| 1995 | PLDI | A Type-Based Compiler for Standard ML. | Zhong Shao, Andrew W. Appel |
| 1994 | PLDI | Separate Compilation for Standard ML. | Andrew W. Appel, David B. MacQueen |
| 1993 | POPL | Smartest Recompilation. | Zhong Shao, Andrew W. Appel |
| 1991 | ASPLOS | Virtual Memory Primitives for User Programs. | Andrew W. Appel, Kai Li |
| 1990 | SIGMETRICS | An Advisor for Flexible Working Sets. | Rafael Alonso, Andrew W. Appel |
| 1989 | POPL | Continuation-Passing, Closure-Passing Style. | Andrew W. Appel, Trevor Jim |
| 1988 | PLDI | Real-time concurrent collection on stock multiprocessors (with retrospective) | Andrew W. Appel |
| 1988 | PLDI | Real-Time Concurrent Collection on Stock Multiprocessors. | Andrew W. Appel, John R. Ellis, Kai Li |
| 1985 | POPL | Semantics-Directed Code Generation. | Andrew W. Appel |