Andrew W. Appel

ORCID

Publication Activity (10 Years)

Years Active: 1985-2024
Publications (10 Years): 30

Top Venues

Proc. ACM Program. Lang.

CoRR

J. Autom. Reason.

CPP

Publications

Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W. Appel, Qinxiang Cao
VST-A: A Foundationally Sound Annotation Verifier. Proc. ACM Program. Lang. 8 (POPL) (2024)
Andrew W. Appel, Ariel Kellison
VCFloat2: Floating-Point Error Analysis in Coq. CPP (2024)
Qinshi Wang, Andrew W. Appel
A Solver for Arrays with Concatenation. J. Autom. Reason. 67 (1) (2023)
Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, Andrew W. Appel
Foundational Verification of Stateful P4 Packet Processing. ITP (2023)
Joshua M. Cohen, Andrew W. Appel
Specifying and Verifying a Real-World Packet Error-Correction System. VSTTE (2023)
Ariel E. Kellison, Andrew W. Appel, Mohit Tekriwal, David Bindel
LAProof: A Library of Formal Proofs of Accuracy and Correctness for Linear Algebra Programs. ARITH (2023)
Mohit Tekriwal, Andrew W. Appel, Ariel E. Kellison, David Bindel, Jean-Baptiste Jeannin
Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method. CICM (2023)
Andrew W. Appel, Xavier Leroy
Efficient Extensional Binary Tries. J. Autom. Reason. 67 (1) (2023)
Joshua M. Cohen, Qinshi Wang, Andrew W. Appel
Verified Erasure Correction in Coq with MathComp and VST. CAV (2) (2022)
Andrew W. Appel
Coq's vibrant ecosystem for verification engineering (invited talk). CPP (2022)
Ariel E. Kellison, Andrew W. Appel
Verified Numerical Methods for Ordinary Differential Equations. NSV/FoMLAS@CAV (2022)
Zoe Paraskevopoulou, John M. Li, Andrew W. Appel
Compositional optimizations for CertiCoq. Proc. ACM Program. Lang. 5 (ICFP) (2021)
Lennart Beringer, Andrew W. Appel
Abstraction and subsumption in modular verification of C programs. Formal Methods Syst. Des. 58 (1-2) (2021)
John M. Li, Andrew W. Appel
Deriving efficient program transformations from rewrite rules. Proc. ACM Program. Lang. 5 (ICFP) (2021)
Andrew W. Appel, Xavier Leroy
Efficient Extensional Binary Tries. CoRR (2021)
Andrew W. Appel, Yves Bertot
Corrigendum: C floating-point proofs layered with VST and Flocq. J. Formaliz. Reason. 13 (1) (2020)
Andrew W. Appel, Yves Bertot
C floating-point proofs layered with VST and Flocq. J. Formaliz. Reason. 13 (1) (2020)
Andrew W. Appel, David A. Naumann
Verified sequential Malloc/Free. ISMM (2020)
William Mansky, Wolf Honoré, Andrew W. Appel
Connecting Higher-Order Separation Logic to a First-Order Outside World. ESOP (2020)
Qinxiang Cao, Shengyi Wang, Aquinas Hobor, Andrew W. Appel
Proof Pearl: Magic Wand as Frame. CoRR (2019)
Zoe Paraskevopoulou, Andrew W. Appel
Closure conversion is safe for space. Proc. ACM Program. Lang. 3 (ICFP) (2019)
Lennart Beringer, Andrew W. Appel
Abstraction and Subsumption in Modular Verification of C Programs. FM (2019)
Andrew W. Appel
Technical Perspective: The scalability of CertiKOS. Commun. ACM 62 (10) (2019)
Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, Andrew W. Appel
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. J. Autom. Reason. 61 (1-4) (2018)
Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, Andrew W. Appel
Verified Correctness and Security of mbedTLS HMAC-DRBG. CoRR (2017)
Olivier Savary Bélanger, Andrew W. Appel
Shrink fast correctly! PPDP (2017)
Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, Andrew W. Appel
Verified Correctness and Security of mbedTLS HMAC-DRBG. CCS (2017)
William Mansky, Andrew W. Appel, Aleksey Nogin
A verified messaging system. Proc. ACM Program. Lang. 1 (OOPSLA) (2017)
Qinxiang Cao, Santiago Cuellar, Andrew W. Appel
Bringing Order to the Separation Logic Jungle. APLAS (2017)
Andrew W. Appel
Modular Verification for Computer Security. CSF (2016)
Andrew W. Appel
Verification of a cryptographic primitive: SHA-256 (abstract). PLDI (2015)
Lennart Beringer, Adam Petcher, Katherine Q. Ye, Andrew W. Appel
Verified Correctness and Security of OpenSSL HMAC. USENIX Security Symposium (2015)
Gordon Stewart, Lennart Beringer, Santiago Cuellar, Andrew W. Appel
Compositional CompCert. POPL (2015)
Andrew W. Appel
Verification of a Cryptographic Primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37 (2) (2015)
Joshua A. Kroll, Gordon Stewart, Andrew W. Appel
Portable Software Fault Isolation. CSF (2014)
Lennart Beringer, Gordon Stewart, Robert Dockins, Andrew W. Appel
Verified Compilation for Shared-Memory C. ESOP (2014)
Josiah Dodds, Andrew W. Appel
Mostly Sound Type System Improves a Foundational Program Verifier. CPP (2013)
Torben Amtoft, Josiah Dodds, Zhi Zhang, Andrew W. Appel, Lennart Beringer, John Hatcliff, Xinming Ou, Andrew Cousino
A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow. POST (2012)
Gordon Stewart, Lennart Beringer, Andrew W. Appel
Verified heap theorem prover by paramodulation. ICFP (2012)
Andrew W. Appel, Robert Dockins, Xavier Leroy
A List-Machine Benchmark for Mechanized Metatheory. J. Autom. Reason. 49 (3) (2012)
Andrew W. Appel
Verified Software Toolchain. NASA Formal Methods (2012)
Gordon Stewart, Andrew W. Appel
Local actions for a curry-style operational semantics. PLPV (2011)
Andrew W. Appel
Security Seals on Voting Machines: A Case Study. ACM Trans. Inf. Syst. Secur. 14 (2) (2011)
Andrew W. Appel
Verified Software Toolchain - (Invited Talk). ESOP (2011)
Andrew W. Appel
VeriSmall: Verified Smallfoot Shape Analysis. CPP (2011)
Aquinas Hobor, Robert Dockins, Andrew W. Appel
A theory of indirection via approximation. POPL (2010)
Amal Ahmed, Andrew W. Appel, Christopher D. Richards, Kedar N. Swadi, Gang Tan, Daniel C. Wang
Semantic foundations for typed assembly languages. ACM Trans. Program. Lang. Syst. 32 (3) (2010)
Sandrine Blazy, Benoît Robillard, Andrew W. Appel
Formal Verification of Coalescing Graph-Coloring Register Allocation. ESOP (2010)
Aquinas Hobor, Robert Dockins, Andrew W. Appel
A Logical Mix of Approximation and Separation. APLAS (2010)
Christian J. Bell, Andrew W. Appel, David Walker
Concurrent Separation Logic for Pipelined Parallelization. SAS (2010)
Andrew W. Appel, Maia Ginsburg, Harri Hursti, Brian W. Kernighan, Christopher D. Richards, Gang Tan, Penny Venetis
The New Jersey Voting-machine Lawsuit and the AVC Advantage DRE Voting Machine. EVT/WOTE (2009)
Robert Dockins, Aquinas Hobor, Andrew W. Appel
A Fresh Look at Separation Algebras and Share Accounting. APLAS (2009)
Robert Dockins, Andrew W. Appel, Aquinas Hobor
Multimodal Separation Logic for Reasoning About Operational Semantics. MFPS (2008)
Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli
Oracle Semantics for Concurrent Separation Logic. ESOP (2008)
Andrew W. Appel, Xavier Leroy
A List-machine Benchmark for Mechanized Metatheory: (Extended Abstract). Electron. Notes Theor. Comput. Sci. 174 (5) (2007)
Andrew W. Appel, Sandrine Blazy
Separation Logic for Small-step Cminor CoRR (2007)
Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, Jérôme Vouillon
A very modal model of a modern, major, general type system. POPL (2007)
Andrew W. Appel, Sandrine Blazy
Separation Logic for Small-Step cminor. TPHOLs (2007)
Gang Tan, Andrew W. Appel, Srimat Chakradhar, Anand Raghunathan, Srivaths Ravi, Daniel C. Wang
Safe Java Native Interface. ISSSE (2006)
Gang Tan, Andrew W. Appel
A Compositional Logic for Control Flow. VMCAI (2006)
Xinming Ou, Sudhakar Govindavajhala, Andrew W. Appel
MulVAL: A Logic-based Network Security Analyzer. USENIX Security Symposium (2005)
Andrew W. Appel, Amy P. Felty
Dependent types ensure partial correctness of theorem provers. J. Funct. Program. 14 (1) (2004)
Gang Tan, Andrew W. Appel, Kedar N. Swadi, Dinghao Wu
Construction of a Semantic Model for a Typed Assembly Language. VMCAI (2004)
Andrew W. Appel, Amy P. Felty
Polymorphic Lemmas and Definitions in lambda-Prolog and Twelf. Theory Pract. Log. Program. 4 (1-2) (2004)
Andrew W. Appel, Amy P. Felty
Polymorphic lemmas and definitions in Lambda Prolog and Twelf CoRR (2004)
Andrew W. Appel
Social processes and proofs of theorems and programs, revisited. PLDI (2004)
Dinghao Wu, Andrew W. Appel, Aaron Stump
Foundational proof checkers with small witnesses. PPDP (2003)
Lujo Bauer, Michael A. Schneider, Edward W. Felten, Andrew W. Appel
Access Control on the Web Using Proof-carrying Authorization. DISCEX (2) (2003)
Juan Chen, Dinghao Wu, Andrew W. Appel, Hai Fang
A provably sound TAL for back-end optimization. PLDI (2003)
Eunyoung Lee, Andrew W. Appel
Policy-enforced linking of untrusted components. ESEC / SIGSOFT FSE (2003)
Lujo Bauer, Andrew W. Appel, Edward W. Felten
Mechanisms for secure modular programming in Java. Softw. Pract. Exp. 33 (5) (2003)
Sudhakar Govindavajhala, Andrew W. Appel
Using Memory Errors to Attack a Virtual Machine. IEEE Symposium on Security and Privacy (2003)
Andrew W. Appel, Neophytos G. Michael, Aaron Stump, Roberto Virga
A Trustworthy Proof Checker. J. Autom. Reason. 31 (3-4) (2003)
Yefim Shuf, Manish Gupta, Hubertus Franke, Andrew W. Appel, Jaswinder Pal Singh
Creating and preserving locality of java applications at allocation and garbage collection times. OOPSLA (2002)
Amal J. Ahmed, Andrew W. Appel, Roberto Virga
A Stratified Semantics of General References A Stratified Semantics of General References. LICS (2002)
Andrew W. Appel, David A. McAllester
An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23 (5) (2001)
Andrew W. Appel, Lal George
Optimal Spilling for CISC Machines with Few Registers. PLDI (2001)
Daniel C. Wang, Andrew W. Appel
Type-preserving garbage collectors. POPL (2001)
Andrew W. Appel
Foundational Proof-Carrying Code. LICS (2001)
Andrew W. Appel, Edward W. Felten
Technological access control interferes with noninfringing scholarship. Commun. ACM 43 (9) (2000)
Dan S. Wallach, Andrew W. Appel, Edward W. Felten
SAFKASI: a security mechanism for language-based systems. ACM Trans. Softw. Eng. Methodol. 9 (4) (2000)
Zhong Shao, Andrew W. Appel
Efficient and safe-for-space closure conversion. ACM Trans. Program. Lang. Syst. 22 (1) (2000)
Andrew W. Appel, Amy P. Felty
A Semantic Model of Types and Machine Instuctions for Proof-Carrying Code. POPL (2000)
Neophytos G. Michael, Andrew W. Appel
Machine Instruction Syntax and Semantics in Higher Order Logic. CADE (2000)
Andrew W. Appel, Amy P. Felty
Lightweight Lemmas in lambda-Prolog. ICLP (1999)
Matthias Blume, Andrew W. Appel
Hierarchical modularity. ACM Trans. Program. Lang. Syst. 21 (4) (1999)
Andrew W. Appel, Edward W. Felten
Proof-Carrying Authentication. CCS (1999)
Jeffrey L. Korn, Andrew W. Appel
Traversal-Based Visualization of Data Structures. INFOVIS (1998)
Andrew W. Appel
SSA is Functional Programming. ACM SIGPLAN Notices 33 (4) (1998)
Matthias Blume, Andrew W. Appel
Lambda-Splitting: A Higher-Order Approach to Cross-Module Optimizations. ICFP (1997)
Daniel C. Wang, Andrew W. Appel, Jeffrey L. Korn, Christopher S. Serra
The Zephyr Abstract Syntax Description Language. DSL (1997)
Andrew W. Appel, Trevor Jim
Shrinking lambda Expressions in Linear Time. J. Funct. Program. 7 (5) (1997)
Andrew W. Appel, Zhong Shao
Empirical and Analytic Study of Stack Versus Heap Cost for Languages with Closures. J. Funct. Program. 6 (1) (1996)
Andrew W. Appel
Intensional Equality ;=) for Continuations. ACM SIGPLAN Notices 31 (2) (1996)
Lal George, Andrew W. Appel
Iterated Register Coalescing. ACM Trans. Program. Lang. Syst. 18 (3) (1996)
Lal George, Andrew W. Appel
Iterated Register Coalescing. POPL (1996)
Andrew P. Tolmach, Andrew W. Appel
A Debugger for Standard ML. J. Funct. Program. 5 (2) (1995)
Marcelo J. R. Gonçalves, Andrew W. Appel
Cache Performance of Fast-Allocating Programs. FPCA (1995)
Zhong Shao, Andrew W. Appel
A Type-Based Compiler for Standard ML. PLDI (1995)
Andrew W. Appel, David B. MacQueen
Separate Compilation for Standard ML. PLDI (1994)

Andrew W. Appel.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Andrew W. Appel