| 2023 | CCS | Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications. | Toby Murray, Mukesh Tiwari, Gidon Ernst, David A. Naumann |
| 2023 | ECOOP | Toward Tool-Independent Summaries for Symbolic Execution. | Frederico Ramos, Nuno Sabino, Pedro Ado, David A. Naumann, Jos Fragoso Santos |
| 2023 | TACAS | The WhyRel Prototype for Modular Relational Verification of Pointer Programs. | Ramana Nagasamudram, Anindya Banerjee, David A. Naumann |
| 2021 | LICS | Alignment Completeness for Relational Hoare Logics. | Ramana Nagasamudram, David A. Naumann |
| 2020 | ICFEM | Type-Based Declassification for Free. | Minh Ngo, David A. Naumann, Tamara Rezk |
| 2020 | ISoLA | Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and History. | David A. Naumann |
| 2017 | POPL | Hypercollecting semantics and its application to static analysis of information flow. | Mounir Assaf, David A. Naumann, Julien Signoles, Eric Totel, Frdric Tronel |
| 2017 | SP | Spartan Jester: End-to-End Information Flow Control for Hybrid Android Applications. | Julian Sexton, Andrey Chudnov, David A. Naumann |
| 2016 | ISoLA | Specifying and Verifying Advanced Control Features. | Gary T. Leavens, David A. Naumann, Hridesh Rajan, Tomoyuki Aotani |
| 2015 | CCS | Inlined Information Flow Monitoring for JavaScript. | Andrey Chudnov, David A. Naumann |
| 2013 | APLAS | Laws of Programming for References. | Giovanny Lucero, David A. Naumann, Augusto Sampaio |
| 2013 | HPCC | Analysis of Authentication and Key Establishment in Inter-generational Mobile Telephony. | Chunyu Tang, David A. Naumann, Susanne Wetzel |
| 2012 | VMCAI | Decision Procedures for Region Logic. | Stan Rosenberg, Anindya Banerjee, David A. Naumann |
| 2011 | SecureComm | Symbolic Analysis for Security of Roaming Protocols in Mobile Networks - [Extended Abstract]. | Chunyu Tang, David A. Naumann, Susanne Wetzel |
| 2010 | ECOOP | Refactoring and representation independence for class hierarchies: extended abstract. | Leila Silva, David A. Naumann, Augusto Sampaio |
| 2010 | ESOP | Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions. | David A. Naumann, Anindya Banerjee |
| 2008 | ECOOP | Regional Logic for Local Reasoning about Global Invariants. | Anindya Banerjee, David A. Naumann, Stan Rosenberg |
| 2008 | SP | Expressive Declassification Policies and Modular Static Enforcement. | Anindya Banerjee, David A. Naumann, Stan Rosenberg |
| 2007 | OOPSLA | Modular verification of higher-order methods with mandatory calls specified by model programs. | Steve M. Shaner, Gary T. Leavens, David A. Naumann |
| 2007 | PLDI | Towards a logical account of declassification. | Anindya Banerjee, David A. Naumann, Stan Rosenberg |
| 2007 | SP | Beyond Stack Inspection: A Unified Access-Control and Information-Flow Security Model. | Marco Pistoia, Anindya Banerjee, David A. Naumann |
| 2006 | ESORICS | From Coupling Relations to Mated Invariants for Checking Information Flow. | David A. Naumann |
| 2006 | SP | Deriving an Information Flow Checker and Certifying Compiler for Java. | Gilles Barthe, Tamara Rezk, David A. Naumann |
| 2005 | ECOOP | State Based Ownership, Reentrance, and Encapsulation. | Anindya Banerjee, David A. Naumann |
| 2005 | FASE | Observational Purity and Encapsulation. | David A. Naumann |
| 2004 | LICS | Towards Imperative Modules: Reasoning about Invariants and Sharing of Mutable State. | David A. Naumann, Michael Barnett |
| 2004 | MPC | Friends Need a Bit More: Maintaining Invariants Over Shared State. | Michael Barnett, David A. Naumann |
| 2004 | SAS | Modular and Constraint-Based Information Flow Inference for an Object-Oriented Language. | Qi Sun, Anindya Banerjee, David A. Naumann |
| 2003 | GLOBECOM | CodeBLUE: a Bluetooth interactive dance club system. | Dennis Hromin, Michael Chladil, Natalie Vanatta, David A. Naumann, Susanne Wetzel, Farooq Anjum, Ravi Jain |
| 2002 | FM | Forward Simulation for Data Refinement of Classes. | Ana Cavalcanti, David A. Naumann |
| 2002 | POPL | Representation independence, confinement and access control [extended abstract]. | Anindya Banerjee, David A. Naumann |
| 2001 | PPDP | Ideal Models for Pointwise Relational and State-Free Imperative Programming. | David A. Naumann |
| 1999 | FM | A Weakest Precondition Semantics for an Object-Oriented Language of Refinement. | Ana Cavalcanti, David A. Naumann |
| 1998 | MPC | Beyond Fun: Order and Membership in Polytypic Imperative Programming. | David A. Naumann |
| 1994 | SIGCSE | Derivation of programs for freshmen. | Richard T. Denman, David A. Naumann, Walter Potter, Gary Richter |