A Commonsense Management Model. - Raymond T. Yeh; David A. Naumann; Roland T. Mittermeir; Reinhard A. Schlemmer; William S. Gilmore; George E. Sumrall; John T. Lebaron (IEEE Softw., 1991)

On the Essence of Oberon. - David A. Naumann (Programming Languages and System Architectures, 1994)

Predicate Transformer Semantics of an Oberon-Like Language. - David A. Naumann (PROCOMET, 1994)

Derivation of programs for freshmen. - Richard T. Denman; David A. Naumann; Walter Potter; Gary Richter (SIGCSE, 1994)

A Recursion Theorem for Predicate Transformers on Inductive Data Types. - David A. Naumann (Inf. Process. Lett., 1994)

Data Refinement, Call by Value and Higher Order Programs. - David A. Naumann (Formal Aspects Comput., 1995)

Predicate Transformers and Higher-Order Programs. - David A. Naumann (Theor. Comput. Sci., 1995)

Beyond Fun: Order and Membership in Polytypic Imperative Programming. - David A. Naumann (MPC, 1998)

Towards squiggly refinement algebra. - David A. Naumann (PROCOMET, 1998)

A Categorical Model for Higher Order Imperative Programming. - David A. Naumann (Math. Struct. Comput. Sci., 1998)

A Weakest Precondition Semantics for an Object-Oriented Language of Refinement. - Ana Cavalcanti 001; David A. Naumann (World Congress on Formal Methods, 1999)

A Weakest Precondition Semantics for Refinement of Object-Oriented Programs. - Ana Cavalcanti 001; David A. Naumann (IEEE Trans. Software Eng., 2000)

Ideal Models for Pointwise Relational and State-Free Imperative Programming. - David A. Naumann (PPDP, 2001)

Calculating sharp adaptation rules. - David A. Naumann (Inf. Process. Lett., 2001)

Predicate transformer semantics of a higher-order imperative language with record subtyping. - David A. Naumann (Sci. Comput. Program., 2001)

Secure Information Flow and Pointer Confinement in a Java-like Language. - Anindya Banerjee 001; David A. Naumann (CSFW, 2002)

Forward Simulation for Data Refinement of Classes. - Ana Cavalcanti 001; David A. Naumann (FME, 2002)

Representation independence, confinement and access control [extended abstract]. - Anindya Banerjee 001; David A. Naumann (POPL, 2002)

Soundness of data refinement for a higher-order imperative language. - David A. Naumann (Theor. Comput. Sci., 2002)

Using Access Control for Secure Information Flow in a Java-like Language. - Anindya Banerjee 001; David A. Naumann (CSFW, 2003)

03411 Final Report - Language Based Security. - Anindya Banerjee 001; Heiko Mantel; David A. Naumann; Andrei Sabelfeld (Language Based Security, 2003)

03411 Abstracts Collection - Language Based Security. - Anindya Banerjee 001; Heiko Mantel; David A. Naumann; Andrei Sabelfeld (Language Based Security, 2003)

CodeBLUE: a Bluetooth interactive dance club system. - Dennis Hromin; Michael Chladil; Natalie Vanatta; David A. Naumann; Susanne Wetzel; Farooq Anjum; Ravi Jain (GLOBECOM, 2003)

History-Based Access Control and Secure Information Flow. - Anindya Banerjee 001; David A. Naumann (CASSIS, 2004)

Friends Need a Bit More: Maintaining Invariants Over Shared State. - Michael Barnett 001; David A. Naumann (MPC, 2004)

Modular and Constraint-Based Information Flow Inference for an Object-Oriented Language. - Qi Sun; Anindya Banerjee 001; David A. Naumann (SAS, 2004)

State Based Ownership, Reentrance, and Encapsulation. - Anindya Banerjee 001; David A. Naumann (ECOOP, 2005)

Verifying a Secure Information Flow Analyzer. - David A. Naumann (TPHOLs, 2005)

Modular Reasoning in Object-Oriented Programming. - David A. Naumann (VSTTE, 2005)

Ownership confinement ensures representation independence for object-oriented programs. - Anindya Banerjee 001; David A. Naumann (J. ACM, 2005)

Stack-based access control and secure information flow. - Anindya Banerjee 001; David A. Naumann (J. Funct. Program., 2005)

Closing Internal Timing Channels by Transformation. - Alejandro Russo; John Hughes 001; David A. Naumann; Andrei Sabelfeld (ASIAN, 2006)

From Coupling Relations to Mated Invariants for Checking Information Flow. - David A. Naumann (ESORICS, 2006)

Allowing State Changes in Specifications. - Michael Barnett 001; David A. Naumann; Wolfram Schulte; Qi Sun (ETRICS, 2006)

Deriving an Information Flow Checker and Certifying Compiler for Java. - Gilles Barthe; Tamara Rezk; David A. Naumann (S&P, 2006)

Category Theoretic Models of Data Refinement. - Michael Johnson; David A. Naumann; John Power (MFCSIT, 2006)

Towards imperative modules: Reasoning about invariants and sharing of mutable state. - David A. Naumann; Michael Barnett 001 (Theor. Comput. Sci., 2006)

Modular verification of higher-order methods with mandatory calls specified by model programs. - Steve M. Shaner; Gary T. Leavens; David A. Naumann (OOPSLA, 2007)

Towards a logical account of declassification. - Anindya Banerjee 001; David A. Naumann; Stan Rosenberg (PLAS, 2007)

Beyond Stack Inspection: A Unified Access-Control and Information-Flow Security Model. - Marco Pistoia; Anindya Banerjee 001; David A. Naumann (S&P, 2007)

On assertion-based encapsulation for object invariants and simulations. - David A. Naumann (Formal Aspects Comput., 2007)

Observational purity and encapsulation. - David A. Naumann (Theor. Comput. Sci., 2007)

Regional Logic for Local Reasoning about Global Invariants. - Anindya Banerjee 001; David A. Naumann; Stan Rosenberg (ECOOP, 2008)

Expressive Declassification Policies and Modular Static Enforcement. - Anindya Banerjee 001; David A. Naumann; Stan Rosenberg (SP, 2008)

Boogie Meets Regions: A Verification Experience Report. - Anindya Banerjee 001; Michael Barnett 001; David A. Naumann (VSTTE, 2008)

Information Flow Monitor Inlining. - Andrey Chudnov; David A. Naumann (CSF, 2010)

Refactoring and representation independence for class hierarchies: extended abstract. - Leila Silva; David A. Naumann; Augusto Sampaio 001 (FTfJP@ECOOP, 2010)

Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions. - David A. Naumann; Anindya Banerjee 001 (ESOP, 2010)

Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients. - Stan Rosenberg; Anindya Banerjee 001; David A. Naumann (VSTTE, 2010)

Symbolic Analysis for Security of Roaming Protocols in Mobile Networks - [Extended Abstract]. - Chunyu Tang; David A. Naumann; Susanne Wetzel (SecureComm, 2011)

Decision Procedures for Region Logic. - Stan Rosenberg; Anindya Banerjee 001; David A. Naumann (VMCAI, 2012)

Refactoring and representation independence for class hierarchies. - David A. Naumann; Augusto Sampaio 001; Leila Silva (Theor. Comput. Sci., 2012)

Laws of Programming for References. - Giovanny Lucero; David A. Naumann; Augusto Sampaio 001 (APLAS, 2013)

A Simple Semantics and Static Analysis for Stack Inspection. - Anindya Banerjee 001; David A. Naumann (Festschrift for Dave Schmidt, 2013)

Analysis of authentication and key establishment in inter-generational mobile telephony. - Chunyu Tang; David A. Naumann; Susanne Wetzel (IACR Cryptol. ePrint Arch., 2013)

Local Reasoning for Global Invariants, Part II: Dynamic Boundaries. - Anindya Banerjee 001; David A. Naumann (J. ACM, 2013)

Local Reasoning for Global Invariants, Part I: Region Logic. - Anindya Banerjee 001; David A. Naumann; Stan Rosenberg (J. ACM, 2013)

State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings. - Anindya Banerjee 001; David A. Naumann (Aliasing in Object-Oriented Programming, 2013)

Information Flow Monitoring as Abstract Interpretation for Relational Logic. - Andrey Chudnov; George Kuan; David A. Naumann (CSF, 2014)

A Logical Analysis of Framing for Specifications with Pure Method Calls. - Anindya Banerjee 001; David A. Naumann (VSTTE, 2014)

Guiding a general-purpose C verifier to prove cryptographic protocols. - François Dupressoir; Andrew D. Gordon 001; Jan Jürjens; David A. Naumann (J. Comput. Secur., 2014)

Inlined Information Flow Monitoring for JavaScript. - Andrey Chudnov; David A. Naumann (CCS, 2015)

Behavioral Subtyping, Specification Inheritance, and Modular Reasoning. - Gary T. Leavens; David A. Naumann (ACM Trans. Program. Lang. Syst., 2015)

Calculational Design of Information Flow Monitors. - Mounir Assaf; David A. Naumann (CSF, 2016)

Relational Logic with Framing and Hypotheses. - Anindya Banerjee 001; David A. Naumann; Mohammad Nikouei (FSTTCS, 2016)

Specifying and Verifying Advanced Control Features. - Gary T. Leavens; David A. Naumann; Hridesh Rajan; Tomoyuki Aotani (ISoLA (2), 2016)

Calculational Design of Information Flow Monitors (extended version). - Mounir Assaf; David A. Naumann (CoRR, 2016)

Relational Logic with Framing and Hypotheses: Technical Report. - Anindya Banerjee 001; David A. Naumann; Mohammad Nikouei (CoRR, 2016)

Towards patterns for heaps and imperative lambdas. - David A. Naumann (J. Log. Algebraic Methods Program., 2016)

Hypercollecting semantics and its application to static analysis of information flow. - Mounir Assaf; David A. Naumann; Julien Signoles; Eric Totel; Frédéric Tronel (POPL, 2017)

An Illustrated Guide to the Model Theory of Supertype Abstraction and Behavioral Subtyping. - Gary T. Leavens; David A. Naumann (SETSS, 2017)

Spartan Jester: End-to-End Information Flow Control for Hybrid Android Applications. - Julian Sexton; Andrey Chudnov; David A. Naumann (IEEE Symposium on Security and Privacy Workshops, 2017)

Assuming You Know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies. - Andrey Chudnov; David A. Naumann (CSF, 2018)

A Logical Analysis of Framing for Specifications with Pure Method Calls. - Anindya Banerjee 001; David A. Naumann; Mohammad Nikouei (ACM Trans. Program. Lang. Syst., 2018)

Whither Specifications as Programs. - David A. Naumann; Minh Ngo (UTP, 2019)

Typed-based Relaxed Noninterference for Free. - Minh Ngo; David A. Naumann; Tamara Rezk (CoRR, 2019)

Whither Programs as Specifications. - David A. Naumann (CoRR, 2019)

Data Abstraction and Relational Program Logic. - Anindya Banerjee 001; Ramana Nagasamudram; David A. Naumann; Mohammad Nikouei (CoRR, 2019)

Type-Based Declassification for Free. - Minh Ngo; David A. Naumann; Tamara Rezk (ICFEM, 2020)

Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and History. - David A. Naumann (ISoLA (2), 2020)

Verified sequential Malloc/Free. - Andrew W. Appel; David A. Naumann (ISMM, 2020)

Alignment Completeness for Relational Hoare Logics. - Ramana Nagasamudram; David A. Naumann (LICS, 2021)

Making Relational Hoare Logic Alignment Complete. - Anindya Banerjee 001; Ramana Nagasamudram; David A. Naumann (CoRR, 2022)

A Relational Program Logic with Data Abstraction and Dynamic Framing. - Anindya Banerjee 001; Ramana Nagasamudram; David A. Naumann; Mohammad Nikouei (ACM Trans. Program. Lang. Syst., 2022)

Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications. - Toby Murray; Mukesh Tiwari; Gidon Ernst; David A. Naumann (CCS, 2023)

Toward Tool-Independent Summaries for Symbolic Execution. - Frederico Ramos; Nuno Sabino; Pedro Adão; David A. Naumann; José Fragoso Santos (ECOOP, 2023)

The WhyRel Prototype for Modular Relational Verification of Pointer Programs. - Ramana Nagasamudram; Anindya Banerjee 001; David A. Naumann (TACAS (2), 2023)

The WhyRel Prototype for Relational Verification. - Ramana Nagasamudram; Anindya Banerjee 001; David A. Naumann (CoRR, 2023)

Alignment complete relational Hoare logics for some and all. - Ramana Nagasamudram; Anindya Banerjee 001; David A. Naumann (CoRR, 2023)

Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version). - Toby Murray; Mukesh Tiwari; Gidon Ernst; David A. Naumann (CoRR, 2023)

Toward Tool-Independent Summaries for Symbolic Execution (Artifact). - Frederico Ramos; Nuno Sabino; Pedro Adão; David A. Naumann; José Fragoso Santos (Dagstuhl Artifacts Ser., 2023)

Special issue: 35th IEEE Computer Security Symposium - CSF 2022. - Stefano Calzavara; David A. Naumann (J. Comput. Secur., 2023)

An Algebra of Alignment for Relational Verification. - Timos Antonopoulos; Eric Koskinen; Ton Chanh Le; Ramana Nagasamudram; David A. Naumann; Minh Ngo (Proc. ACM Program. Lang., 2023)

Verifying a C Implementation of Derecho's Coordination Mechanism Using VST and Coq. - Ramana Nagasamudram; Lennart Beringer; Ken Birman; Mae Milano; David A. Naumann (NFM, 2024)

Verifying a C implementation of Derecho's coordination mechanism using VST and Coq (artifact). - Ramana Nagasamudram; Lennart Beringer; Ken Birman; Mae Milano; David A. Naumann (Zenodo, 2024)