David A. Naumann

ORCID

Publication Activity (10 Years)

Years Active: 1991-2024
Publications (10 Years): 35

Top Venues

CoRR

CSF

ACM Trans. Program. Lang. Syst.

ISoLA (2)

Publications

Ramana Nagasamudram, Lennart Beringer, Ken Birman, Mae Milano, David A. Naumann
Verifying a C Implementation of Derecho's Coordination Mechanism Using VST and Coq. NFM (2024)
Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
The WhyRel Prototype for Relational Verification. CoRR (2023)
Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, José Fragoso Santos
Toward Tool-Independent Summaries for Symbolic Execution. ECOOP (2023)
Toby Murray, Mukesh Tiwari, Gidon Ernst, David A. Naumann
Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version). CoRR (2023)
Toby Murray, Mukesh Tiwari, Gidon Ernst, David A. Naumann
Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications. CCS (2023)
Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, Minh Ngo
An Algebra of Alignment for Relational Verification. Proc. ACM Program. Lang. 7 (POPL) (2023)
Stefano Calzavara, David A. Naumann
Special issue: 35th IEEE Computer Security Symposium - CSF 2022. J. Comput. Secur. 31 (5) (2023)
Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
The WhyRel Prototype for Modular Relational Verification of Pointer Programs. TACAS (2) (2023)
Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
Alignment complete relational Hoare logics for some and all. CoRR (2023)
Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, José Fragoso Santos
Toward Tool-Independent Summaries for Symbolic Execution (Artifact). Dagstuhl Artifacts Ser. 9 (2) (2023)
Anindya Banerjee, Ramana Nagasamudram, David A. Naumann, Mohammad Nikouei
A Relational Program Logic with Data Abstraction and Dynamic Framing. ACM Trans. Program. Lang. Syst. 44 (4) (2022)
Anindya Banerjee, Ramana Nagasamudram, David A. Naumann
Making Relational Hoare Logic Alignment Complete. CoRR (2022)
Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, Minh Ngo
An algebra of alignment for relational verification. CoRR (2022)
Ramana Nagasamudram, David A. Naumann
Alignment Completeness for Relational Hoare Logics. LICS (2021)
Ramana Nagasamudram, David A. Naumann
Alignment Completeness for Relational Hoare Logics. CoRR (2021)
David A. Naumann
Thirty-seven years of relational Hoare logic: remarks on its principles and history. CoRR (2020)
Minh Ngo, David A. Naumann, Tamara Rezk
Type-Based Declassification for Free. ICFEM (2020)
David A. Naumann
Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and History. ISoLA (2) (2020)
Andrew W. Appel, David A. Naumann
Verified sequential Malloc/Free. ISMM (2020)
Minh Ngo, David A. Naumann, Tamara Rezk
Typed-based Relaxed Noninterference for Free. CoRR (2019)
David A. Naumann, Minh Ngo
Whither Specifications as Programs. UTP (2019)
David A. Naumann
Whither Programs as Specifications. CoRR (2019)
Mohammad Nikouei, Anindya Banerjee, David A. Naumann
Data Abstraction and Relational Program Logic. CoRR (2019)
Anindya Banerjee, David A. Naumann, Mohammad Nikouei
A Logical Analysis of Framing for Specifications with Pure Method Calls. ACM Trans. Program. Lang. Syst. 40 (2) (2018)
Andrey Chudnov, David A. Naumann
Assuming You Know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies. CSF (2018)
Julian Sexton, Andrey Chudnov, David A. Naumann
Spartan Jester: End-to-End Information Flow Control for Hybrid Android Applications. IEEE Symposium on Security and Privacy Workshops (2017)
Gary T. Leavens, David A. Naumann
An Illustrated Guide to the Model Theory of Supertype Abstraction and Behavioral Subtyping. SETSS (2017)
Mounir Assaf, David A. Naumann, Julien Signoles, Eric Totel, Frédéric Tronel
Hypercollecting semantics and its application to static analysis of information flow. POPL (2017)
Anindya Banerjee, David A. Naumann, Mohammad Nikouei
Relational Logic with Framing and Hypotheses: Technical Report. CoRR (2016)
Mounir Assaf, David A. Naumann
Calculational Design of Information Flow Monitors. CSF (2016)
David A. Naumann
Towards patterns for heaps and imperative lambdas. J. Log. Algebraic Methods Program. 85 (5) (2016)
Mounir Assaf, David A. Naumann, Julien Signoles, Eric Totel, Frédéric Tronel
Hypercollecting Semantics and its Application to Static Analysis of Information Flow. CoRR (2016)
Mounir Assaf, David A. Naumann
Calculational Design of Information Flow Monitors (extended version). CoRR (2016)
Gary T. Leavens, David A. Naumann, Hridesh Rajan, Tomoyuki Aotani
Specifying and Verifying Advanced Control Features. ISoLA (2) (2016)
Anindya Banerjee, David A. Naumann, Mohammad Nikouei
Relational Logic with Framing and Hypotheses. FSTTCS (2016)
David A. Naumann
Towards Patterns for Heaps and Imperative Lambdas. CoRR (2015)
Andrey Chudnov, David A. Naumann
Inlined Information Flow Monitoring for JavaScript. CCS (2015)
Gary T. Leavens, David A. Naumann
Behavioral Subtyping, Specification Inheritance, and Modular Reasoning. ACM Trans. Program. Lang. Syst. 37 (4) (2015)
Andrey Chudnov, George Kuan, David A. Naumann
Information Flow Monitoring as Abstract Interpretation for Relational Logic. CSF (2014)
Anindya Banerjee, David A. Naumann
A Logical Analysis of Framing for Specifications with Pure Method Calls. VSTTE (2014)
François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann
Guiding a general-purpose C verifier to prove cryptographic protocols. J. Comput. Secur. 22 (5) (2014)
Anindya Banerjee, David A. Naumann
A Simple Semantics and Static Analysis for Stack Inspection. Festschrift for Dave Schmidt (2013)
François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols. CoRR (2013)
Giovanny Lucero, David A. Naumann, Augusto Sampaio
Laws of Programming for References. APLAS (2013)
Anindya Banerjee, David A. Naumann, Stan Rosenberg
Local Reasoning for Global Invariants, Part I: Region Logic. J. ACM 60 (3) (2013)
Chunyu Tang, David A. Naumann, Susanne Wetzel
Analysis of Authentication and Key Establishment in Inter-generational Mobile Telephony. HPCC/EUC (2013)
Chunyu Tang, David A. Naumann, Susanne Wetzel
Analysis of authentication and key establishment in inter-generational mobile telephony. IACR Cryptol. ePrint Arch. 2013 (2013)
Anindya Banerjee, David A. Naumann
Local Reasoning for Global Invariants, Part II: Dynamic Boundaries. J. ACM 60 (3) (2013)
Stan Rosenberg, Anindya Banerjee, David A. Naumann
Decision Procedures for Region Logic. VMCAI (2012)
David A. Naumann, Augusto Sampaio, Leila Silva
Refactoring and representation independence for class hierarchies. Theor. Comput. Sci. 433 (2012)
Chunyu Tang, David A. Naumann, Susanne Wetzel
Symbolic Analysis for Security of Roaming Protocols in Mobile Networks - [Extended Abstract]. SecureComm (2011)
François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols. CSF (2011)
Leila Silva, David A. Naumann, Augusto Sampaio
Refactoring and representation independence for class hierarchies: extended abstract. FTfJP@ECOOP (2010)
David A. Naumann, Anindya Banerjee
Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions. ESOP (2010)
Andrey Chudnov, David A. Naumann
Information Flow Monitor Inlining. CSF (2010)
Stan Rosenberg, Anindya Banerjee, David A. Naumann
Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients. VSTTE (2010)
Michael Johnson, David A. Naumann, John Power
Category Theoretic Models of Data Refinement. Electron. Notes Theor. Comput. Sci. 225 (2009)
Anindya Banerjee, David A. Naumann, Stan Rosenberg
Expressive Declassification Policies and Modular Static Enforcement. IEEE Symposium on Security and Privacy (2008)
Anindya Banerjee, Michael Barnett, David A. Naumann
Boogie Meets Regions: A Verification Experience Report. VSTTE (2008)
Anindya Banerjee, David A. Naumann, Stan Rosenberg
Regional Logic for Local Reasoning about Global Invariants. ECOOP (2008)
Marco Pistoia, Anindya Banerjee, David A. Naumann
Beyond Stack Inspection: A Unified Access-Control and Information-Flow Security Model. IEEE Symposium on Security and Privacy (2007)
David A. Naumann
On assertion-based encapsulation for object invariants and simulations. Formal Aspects Comput. 19 (2) (2007)
Anindya Banerjee, David A. Naumann, Stan Rosenberg
Towards a logical account of declassification. PLAS (2007)
Steve M. Shaner, Gary T. Leavens, David A. Naumann
Modular verification of higher-order methods with mandatory calls specified by model programs. OOPSLA (2007)
David A. Naumann
Observational purity and encapsulation. Theor. Comput. Sci. 376 (3) (2007)
Gilles Barthe, Tamara Rezk, David A. Naumann
Deriving an Information Flow Checker and Certifying Compiler for Java. IEEE Symposium on Security and Privacy (2006)
Michael Barnett, David A. Naumann, Wolfram Schulte, Qi Sun
Allowing State Changes in Specifications. ETRICS (2006)
David A. Naumann, Michael Barnett
Towards imperative modules: Reasoning about invariants and sharing of mutable state. Theor. Comput. Sci. 365 (1-2) (2006)
Alejandro Russo, John Hughes, David A. Naumann, Andrei Sabelfeld
Closing Internal Timing Channels by Transformation. ASIAN (2006)
David A. Naumann
From Coupling Relations to Mated Invariants for Checking Information Flow. ESORICS (2006)
Anindya Banerjee, David A. Naumann
State Based Ownership, Reentrance, and Encapsulation. ECOOP (2005)
David A. Naumann
Verifying a Secure Information Flow Analyzer. TPHOLs (2005)
David A. Naumann
Modular Reasoning in Object-Oriented Programming. VSTTE (2005)
Anindya Banerjee, David A. Naumann
Stack-based access control and secure information flow. J. Funct. Program. 15 (2) (2005)
Anindya Banerjee, David A. Naumann
Ownership confinement ensures representation independence for object-oriented programs. J. ACM 52 (6) (2005)
David A. Naumann
Observational Purity and Encapsulation. FASE (2005)
David A. Naumann, Michael Barnett
Towards Imperative Modules: Reasoning about Invariants and Sharing of Mutable State. LICS (2004)
Anindya Banerjee, David A. Naumann
History-Based Access Control and Secure Information Flow. CASSIS (2004)
Qi Sun, Anindya Banerjee, David A. Naumann
Modular and Constraint-Based Information Flow Inference for an Object-Oriented Language. SAS (2004)
David A. Naumann
Assertion-Based Encapsulation, Object Invariants and Simulations. FMCO (2004)
Michael Barnett, David A. Naumann
Friends Need a Bit More: Maintaining Invariants Over Shared State. MPC (2004)
Anindya Banerjee, David A. Naumann
Using Access Control for Secure Information Flow in a Java-like Language. CSFW (2003)
Anindya Banerjee, Heiko Mantel, David A. Naumann, Andrei Sabelfeld
03411 Abstracts Collection - Language Based Security. Language Based Security (2003)
Dennis Hromin, Michael Chladil, Natalie Vanatta, David A. Naumann, Susanne Wetzel, Farooq Anjum, Ravi Jain
CodeBLUE: a Bluetooth interactive dance club system. GLOBECOM (2003)
Anindya Banerjee, Heiko Mantel, David A. Naumann, Andrei Sabelfeld
03411 Final Report - Language Based Security. Language Based Security (2003)
Anindya Banerjee, David A. Naumann
Ownership Confinement Ensures Representation Independence for Object-Oriented Programs CoRR (2002)
Ana Cavalcanti, David A. Naumann
Forward Simulation for Data Refinement of Classes. FME (2002)
David A. Naumann
Soundness of data refinement for a higher-order imperative language. Theor. Comput. Sci. 278 (1-2) (2002)
Anindya Banerjee, David A. Naumann
Secure Information Flow and Pointer Confinement in a Java-like Language. CSFW (2002)
Anindya Banerjee, David A. Naumann
Representation independence, confinement and access control [extended abstract]. POPL (2002)
David A. Naumann
Ideal Models for Pointwise Relational and State-Free Imperative Programming. PPDP (2001)
David A. Naumann
Predicate transformer semantics of a higher-order imperative language with record subtyping. Sci. Comput. Program. 41 (1) (2001)
David A. Naumann
Calculating sharp adaptation rules. Inf. Process. Lett. 77 (2-4) (2001)
Ana Cavalcanti, David A. Naumann
A Weakest Precondition Semantics for Refinement of Object-Oriented Programs. IEEE Trans. Software Eng. 26 (8) (2000)
Ana Cavalcanti, David A. Naumann
A Weakest Precondition Semantics for an Object-Oriented Language of Refinement. World Congress on Formal Methods (1999)
David A. Naumann
A Categorical Model for Higher Order Imperative Programming. Math. Struct. Comput. Sci. 8 (4) (1998)
David A. Naumann
Towards squiggly refinement algebra. PROCOMET (1998)
David A. Naumann
Beyond Fun: Order and Membership in Polytypic Imperative Programming. MPC (1998)
David A. Naumann
Predicate Transformers and Higher-Order Programs. Theor. Comput. Sci. 150 (1) (1995)
David A. Naumann
Data Refinement, Call by Value and Higher Order Programs. Formal Aspects Comput. 7 (6) (1995)

David A. Naumann.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

David A. Naumann