• 3786 Citations
  • 31 h-Index
1985 …2020

Research output per year

If you made any changes in Pure these will be visible here soon.

Research Output

2020

Connecting Higher-Order Separation Logic to a First-Order Outside World

Mansky, W., Honoré, W. & Appel, A. W., 2020, Programming Languages and Systems- 29th European Symposium on Programming, ESOP 2020 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings. Müller, P. (ed.). Springer, p. 428-455 28 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12075 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Open Access

Verified sequential Malloc/Free

Appel, A. W. & Naumann, D. A., Jun 16 2020, ISMM 2020 - Proceedings of the 2020 ACM SIGPLAN International Symposium on Memory Management, co-located with PLDI 2020. Ding, C. & Maas, M. (eds.). Association for Computing Machinery, p. 48-59 12 p. (International Symposium on Memory Management, ISMM).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Open Access
2019

Abstraction and subsumption in modular verification of C programs

Beringer, L. & Appel, A. W., Jan 1 2019, Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings. ter Beek, M. H., McIver, A. & Oliveira, J. N. (eds.). Springer, p. 573-590 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11800 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Technical perspective the scalability of certikos

Appel, A. W., Oct 2019, In : Communications of the ACM. 62, 10, p. 88 1 p.

Research output: Contribution to journalComment/debate

Open Access

You can publish it! (You have to)

Appel, A. W., Nov 2019, In : Communications of the ACM. 62, 11, 1 p.

Research output: Contribution to journalLetter

Open Access
2018

VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs

Cao, Q., Beringer, L., Gruetter, S., Dodds, J. & Appel, A. W., Jun 1 2018, In : Journal of Automated Reasoning. 61, 1-4, p. 367-422 56 p.

Research output: Contribution to journalArticle

16 Scopus citations
2017

Bringing order to the separation logic jungle

Cao, Q., Cuellar, S. & Appel, A. W., Jan 1 2017, Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Proceedings. Chang, B-Y. E. (ed.). Springer Verlag, p. 190-211 22 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10695 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

Position paper: the science of deep specification

Appel, A. W., Beringer, L., Chlipala, A., Pierce, B. C., Shao, Z., Weirich, S. & Zdancewic, S., Oct 13 2017, In : Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences. 375, 2104, 20160331.

Research output: Contribution to journalArticle

10 Scopus citations

Shrink fast correctly!

Bélanger, O. S. & Appel, A. W., Oct 9 2017, Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, PPDP 2017. Association for Computing Machinery, p. 49-60 12 p. (ACM International Conference Proceeding Series; vol. Part F131196).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Verified correctness and security of mbed TLS HMAC-DRBG

Ye, K. Q., Green, M., Sanguansin, N., Beringer, L., Petcher, A. & Appel, A. W., Oct 30 2017, CCS 2017 - Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, p. 2007-2020 14 p. (Proceedings of the ACM Conference on Computer and Communications Security).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

20 Scopus citations
2016

Modular verification for computer security

Appel, A. W., Aug 8 2016, Proceedings - IEEE 29th Computer Security Foundations Symposium, CSF 2016. IEEE Computer Society, 7536361. (Proceedings - IEEE Computer Security Foundations Symposium; vol. 2016-August).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Scopus citations
2015

Compositional CompCert

Stewart, G., Beringer, L., Cuellar, S. & Appel, A. W., Jan 2015, In : ACM SIGPLAN Notices. 50, 1, p. 275-287 13 p.

Research output: Contribution to journalArticle

4 Scopus citations

Compositional comp cert

Stewart, G., Beringer, L., Cuellar, S. & Appel, A. W., Jan 14 2015, POPL 2015 - Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for Computing Machinery, p. 275-287 13 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages; vol. 2015-January).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

30 Scopus citations

Verification of a cryptographic primitive: SHA-256 7

Appel, A. W., Apr 1 2015, In : ACM Transactions on Programming Languages and Systems. 37, 2, 7.

Research output: Contribution to journalArticle

53 Scopus citations

Verification of a cryptographic primitive: SHA-256 (abstract)

Appel, A. W., Jun 3 2015, PLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery, Vol. 2015-June. 1 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Verified correctness and security of OpenSSL HMAC

Beringer, L., Petcher, A., Ye, K. Q. & Appel, A. W., Jan 1 2015, Proceedings of the 24th USENIX Security Symposium. USENIX Association, p. 207-221 15 p. (Proceedings of the 24th USENIX Security Symposium).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

47 Scopus citations
2014

Portable software fault isolation

Kroll, J. A., Stewart, G. & Appel, A. W., Nov 13 2014, Proceedings - 2014 IEEE 27th Computer Security Foundations Symposium, CSF 2014. IEEE Computer Society, p. 18-32 15 p. 6957100. (Proceedings of the Computer Security Foundations Workshop; vol. 2014-January).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Scopus citations

Program logics for certified compilers

Appel, A. W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S. & Leroy, X., Jan 1 2014, Cambridge University Press. 451 p.

Research output: Book/ReportBook

72 Scopus citations

Verified compilation for shared-memory C

Beringer, L., Stewart, G., Dockins, R. & Appel, A. W., Jan 1 2014, Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. Springer Verlag, p. 107-127 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8410 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Scopus citations
2013

Mostly sound type system improves a foundational program verifier

Dodds, J. & Appel, A. W., Dec 1 2013, Certified Programs and Proofs - Third International Conference, CPP 2013, Proceedings. p. 17-32 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8307 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations
2012

A certificate infrastructure for machine-checked proofs of conditional information flow

Amtoft, T., Dodds, J., Zhang, Z., Appel, A., Beringer, L., Hatcliff, J., Ou, X. & Cousino, A., Apr 9 2012, Principles of Security and Trust - First International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. p. 369-389 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7215 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

15 Scopus citations

A list-machine benchmark for mechanized metatheory

Appel, A. W., Dockins, R. & Leroy, X., Oct 1 2012, In : Journal of Automated Reasoning. 49, 3, p. 453-491 39 p.

Research output: Contribution to journalArticle

4 Scopus citations

Creating and preserving locality of Java applications at allocation and garbage collection times

Shuf, Y., Gupta, M., Franke, H., Appel, A. W. & Singh, J. P., Nov 2012, In : ACM SIGPLAN Notices. 37, 11, p. 13-25 13 p.

Research output: Contribution to journalArticle

Verified heap theorem prover by paramodulation

Stewart, G., Beringer, L. & Appel, A. W., Oct 22 2012, ICFP'12 - Proceedings of the 2012 ACM SIGPLAN International Conference on Functional Programming. p. 3-14 12 p. (Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Scopus citations

Verified heap theorem prover by paramodulation

Stewart, G., Beringer, L. & Appel, A. W., Sep 1 2012, In : ACM SIGPLAN Notices. 47, 9, p. 3-14 12 p.

Research output: Contribution to journalArticle

1 Scopus citations
2011

Local actions for a curry-style operational semantics

Stewart, G. & Appel, A. W., 2011, PLPV'11 - Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification. p. 31-42 12 p. (PLPV'11 - Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

Security seals on voting machines: A case study

Appel, A. W., Sep 2011, In : ACM Transactions on Information and System Security. 14, 2, 18.

Research output: Contribution to journalArticle

10 Scopus citations

Verified software toolchain (Invited talk)

Appel, A. W., Apr 4 2011, Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings. p. 1-17 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6602 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

65 Scopus citations

VeriSmall: Verified smallfoot shape analysis

Appel, A. W., Nov 28 2011, Certified Programs and Proofs - First International Conference, CPP 2011, Proceedings. p. 231-246 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7086 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations
2010

A logical mix of approximation and separation

Hobor, A., Dockins, R. & Appel, A. W., Dec 1 2010, Programming Languages and Systems - 8th Asian Symposium, APLAS 2010, Proceedings. p. 439-454 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6461 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

A theory of indirection via approximation

Hobor, A., Dockinsy, R. & Appel, A. W., Jan 2010, In : ACM SIGPLAN Notices. 45, 1, p. 171-184 14 p.

Research output: Contribution to journalArticle

6 Scopus citations

A theory of indirection via approximation

Hobor, A., Dockins, R. & Appel, A. W., Apr 20 2010, POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 171-184 14 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

13 Scopus citations

Concurrent separation logic for pipelined parallelization

Bell, C. J., Appel, A. W. & Walker, D., Nov 12 2010, Static Analysis - 17th International Symposium, SAS 2010, Proceedings. p. 151-166 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6337 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Scopus citations

Semantic foundations for typed assembly languages

Ahmed, A., Appel, A. W., Richards, C. D., Swadi, K. N., Tan, G. & Wang, D. C., Mar 1 2010, In : ACM Transactions on Programming Languages and Systems. 32, 3, 1709094.

Research output: Contribution to journalArticle

14 Scopus citations
2009

A fresh look at separation algebras and share accounting

Dockins, R., Hobor, A. & Appel, A. W., Dec 28 2009, Programming Languages and Systems - 7th Asian Symposium, APLAS 2009, Proceedings. p. 161-177 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5904 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

67 Scopus citations
2008

Multimodal Separation Logic for Reasoning About Operational Semantics

Dockins, R., Appel, A. W. & Hobor, A., Oct 22 2008, In : Electronic Notes in Theoretical Computer Science. 218, C, p. 5-20 16 p.

Research output: Contribution to journalArticle

5 Scopus citations

Oracle semantics for concurrent separation logic

Hobor, A., Appel, A. W. & Nardelli, F. Z., Jul 21 2008, Programming Languages and Systems - 17th European Symposium on Programming, ESOP 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings. p. 353-367 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4960 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

66 Scopus citations
2007

A List-machine Benchmark for Mechanized Metatheory. (Extended Abstract)

Appel, A. W. & Leroy, X., Jun 2 2007, In : Electronic Notes in Theoretical Computer Science. 174, 5, p. 95-108 14 p.

Research output: Contribution to journalArticle

4 Scopus citations

A very modal model of a modern, major, general type system

Appel, A. W., Melliès, P. A., Richards, C. D. & Vouillon, J., Jan 2007, In : ACM SIGPLAN Notices. 42, 1, p. 109-122 14 p.

Research output: Contribution to journalArticle

25 Scopus citations

A very modal model of a modern, major, general type system

Appel, A. W., Melliès, P. A., Richards, C. D. & Vouillon, J., Sep 3 2007, Conference Record of POPL 2007: The 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Papers Presented at the Symposium. p. 109-122 14 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

44 Scopus citations

Separation logic for small-step Cminor

Appel, A. W. & Blazy, S., 2007, Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings. Springer Verlag, p. 5-21 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4732 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

49 Scopus citations
2006

A compositional logic for control flow

Tan, G. & Appel, A. W., Jul 6 2006, Verification, Model Checking, and Abstract Interpretation - 7th International Conference, VMCAI 2006, Proceedings. p. 80-94 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 3855 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

28 Scopus citations
2005

MulVAL: A logic-based network security analyzer

Ou, X., Govindavajhala, S. & Appel, A. W., Jan 1 2005, p. 113-128. 16 p.

Research output: Contribution to conferencePaper

MulVAL: A logic-based network security analyzer

Ou, X., Govindavajhala, S. & Appel, A. W., Jan 1 2005, p. 113-128. 16 p.

Research output: Contribution to conferencePaper

332 Scopus citations
2004

Construction of a semantic model for a typed assembly language

Tan, G., Appel, A. W., Swadi, K. N. & Wu, D., Jan 1 2004, Verification, Model Checking, and Abstract Interpretation - 5th International Conference, VMCAI 2004, Proceedings. Steffen, B. & Levi, G. (eds.). Springer Verlag, p. 30-43 14 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 2937).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Scopus citations

Dependent types ensure partial correctness of theorem provers

Appel, A. W. & Felty, A. P., Jan 1 2004, In : Journal of Functional Programming. 14, 1, p. 3-19 17 p.

Research output: Contribution to journalArticle

14 Scopus citations

Polymorphic lemmas and definitions in λProlog and Twelf

Appel, A. W. & Felty, A. P., Jan 1 2004, In : Theory and Practice of Logic Programming. 4, 1-2, p. 1-39 39 p.

Research output: Contribution to journalArticle

3 Scopus citations

Real-time concurrent collection on stock multiprocessors

Appel, A. W., Apr 1 2004, In : ACM SIGPLAN Notices. 39, 4, p. 205-206 2 p.

Research output: Contribution to journalArticle

1 Scopus citations

Real-time concurrent collection on stock multiprocessors

Appel, A. W., Ellis, J. R. & Li, K., Apr 1 2004, In : ACM SIGPLAN Notices. 39, 4, p. 207-216 10 p.

Research output: Contribution to journalArticle

1 Scopus citations
2003

Access control on the Web using proof-carrying authorization

Bauer, L., Schneider, M. A., Felten, E. W. & Appel, A. W., Jan 1 2003, Proceedings - DARPA Information Survivability Conference and Exposition, DISCEX 2003. Institute of Electrical and Electronics Engineers Inc., p. 117-119 3 p. 1194942. (Proceedings - DARPA Information Survivability Conference and Exposition, DISCEX 2003; vol. 2).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Scopus citations