David Naumann

Building: North Building
Room: 309
Phone: +1 (201) 216-5608
Email: dnaumann@stevens.edu

Ph.D., Computer Science, University of Texas at Austin, 1992 (PhD supervisors: Edsger W. Dijkstra and C.A.R. Hoare)

B.A., Computer Science, University of Texas at Austin, 1982 


Formal methods and security, including: fine-grained confidentiality/integrity policies; automated analysis/transformation of programs combined with access control to enforce such policies; use of program verification technology for security; methodology for formal specification of system components and refactoring of implementations.


General Information

More complete information can be found via my home page and search sites such as Google Scholar and DBLP.


Programmer-designer, IBM, 1982-85

Consultant-programmer, Renaissance Systems, 1985-86

Associate Scientist, International Software Systems, 1986-91

Assistant Professor, Southwestern University, 1991-97

Visiting Researcher, Microsoft Research Cambridge, Fall 2010

Research Professor, IMDEA Software Institute, Madrid, Spring 2011

Visiting Fellow, Princeton University, 2017-18


Professional Service

Chair, Unifying Theories of Programming (5th International Symposium, 2014).

Co-chair of Formal Methods: Foundations and Applications (15th Brazilian Symposium, 2012).

Co-chair of 2009 ACM Workshop on Programming Languages and Analysis for Security.

Verified Software Initiative: chair of Theory Panel, co-chair of 2008 VSTTE workshop, co-chair of 2010 VSTTE workshop.

Member of the Technical Committees for numerous IEEE and ACM research conferences and workshops.


Consulting Service

Microsoft Research

Vulcan Inc.

Galois Inc.


Honors & Awards

Best Software Sciences paper, ETAPS 2005.

Davis Memorial Award for Research Excellence, 2006.

Best student paper (coauthor), OOPSLA 2007.

Distinguished paper, ECOOP 2008.

Invited keynote speaker, ETAPS 2010.

Invited keynote speaker, IBM Programming Languages Day 2015.


Professor of Computer Science since 2008
Associate Professor of Computer Science 2002-08
Assistant Professor of Computer Science 1997-2002
Professional Societies

Member ACM, IEEE.


Grants, Contracts & Funds

NSF award INT-9813854: Towards a Practical Calculus of Object-Oriented Programming.

NSF award CCR-0208984: Integrating Confinement and Access Control for Encapsulation.

NSF award CCF-0429894: Formal Methods for Behavioral Subclassing and Callbacks.

NSF award CNS-0627338: Access Control and Downgrading in Information Flow Assurance.

NSF award CNS-0708330: A JML Community Infrastructure --Revitalizing Tools and Documentation to Aid Formal Methods Research.

NSF award DUE-083084: Scholarship for Service Cybersecurity Scholars Program (co-PI).

NSF award CCF-0915611: Specification Language Foundations for Modular Reasoning Methodologies.

DHS Science and Technology (subcontract): Tunable Information Flow.

NSF award CNS-1228930: Flexible and Practical Information Flow Assurance for Mobile Apps.

NSF award CCF-1649884: Hyperproperty Abstraction for Information Flow Control

NSF award CNS 1718713: Relational Verification for Information Assurance and Privacy.


Selected Publications
  1. Anindya Banerjee, David Naumann, Mohammad Nikouei. (2018). "A Logical Analysis of Framing for Specifications with Pure Method Calls", Transactions on Programming Languages and Systems, ACM Press. 40 (2), 6:1-6:90.
  2. Gary Leavens and David Naumann. (Aug 2015). "Behavioral Subtyping, Specification Inheritance, and Modular Reasoning", Transactions on Programming Languages and Systems, ACM Press. 37 (4), 13:1-13:88.
  3. Francois Dupressoir, Andrew D. Gordon, Jan Jurjens, David A Naumann. (2014). "Guiding a general-purpose C verifier to prove cryptographic protocols", Journal of Computer Security.
  4. Anindya Banerjee, David A. Naumann. (Jun 2013). "Local Reasoning for Global Invariants, Part II: Dynamic Boundaries", Journal of the ACM, ACM Press. 60 (3), 19:1-19:73.  Local Reasoning for Global Invariants, Part II: Dynamic Boundaries  .
  5. Anindya Banerjee, David A. Naumann, Stan Rosenberg. (Jun 2013). "Local Reasoning for Global Invariants, Part I: Region Logic", Journal of the ACM, ACM Press. 60 (3), 18:1-18:56.  Local Reasoning for Global Invariants, Part I: Region Logic  .
  6. David Naumann, Augusto Sampaio, and Leila Silva. (2012). "Refactoring and Representation Independence for Class Hierarchies", Theoretical Computer Science, 433 60-97.
Conference Proceedings
  1. Andrey Chudnov and David Naumann. (Jun 2018). "Assuming You Know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies", Computer Security Foundations. IEEE. 189-203.
  2. Mounir Assaf, David Naumann, Julien Signoles, Eric Totel, Frederic Tronel. (Jan 2017). "Hypercollecting semantics and its application to static analysis of information flow", ACM Symposium on Principles of Programming Languages (POPL). ACM Press.
  3. Mounir Assaf and David Naumann. (Jun 2016). "Calculational Design of Information Flow Monitors", IEEE Computer Security Foundations Symposium. IEEE Press. 210-224.
  4. Andrey Chudnov and David Naumann. (Oct 2015). "Information Flow Monitoring for JavaScript", Computer and Communications Security (CCS). ACM Press. 629-643.
  5. Andrey Chudnov, George Kuan, David Naumann. (Jul 2014). "Information flow monitoring as abstract interpretation for relational logic", Computer Security Foundations Symposium. Anupan Datta and Cedric Fournet, IEEE Press.
  6. Chunyu Tang, David Naumann, Susanne Wetzel. (Nov 2013). "Analysis of authentication and key establishment in inter-generational mobile telephony", International Symposium on Trust, Security, and Privacy for Emerging Applications.
  7. Stan Rosenberg, Anindya Banerjee, David A Naumann. (Jan 2012). "Decision Procedures for Region Logic", 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer. pages 379-395, vol 7148 of Lecture Notes in Computer Science. 7148 379-395.
  8. François Dupressoir, Andrew D. Gordon, Jan Jurjens, and David A.Naumann. (2011). "Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols", In Proceedings, IEEE Computer Security Foundations Symposium.
  9. David A Naumann and Anindya Banerjee. (Mar 2010). "Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions", European Symposium on Programming . Andrew Gordon, Springer LNCS. 6012 2-22.
  10. Anindya Banerje and Mike Barnett and David Naumann. (Oct 2008). "Boogie Meets Regions: a Verification Experience Report", Verified Software: Theories, Tools, Experiments (VSTTE). 177-191.
  11. Anindya Banerjee and David Naumann and Stan Rosenberg. (Jul 2008). "Regional Logic for Local Reasoning about Global Invariants", European Conference on Object-Oriented Programming (ECOOP). 387-411.
  12. Anindya Banerjee and David Naumann and Stan Rosenberg. (May 2008). "Expressive Declassification Policies and Modular Static Enforcement", IEEE Symposium on Security and Privacy. IEEE Press. 339-353.
  13. Andrey Chudnov and David A Naumann. (Jun 2010). "Information Flow Monitor Inlining", Computer Security Foundations Symposium. IEEE Press.
Book Chapters
  1. Anindya Banerjee, David A. Naumann. (2013). "State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings", Aliasing in Object-Oriented Programming (State of the Art Survey), Dave Clarke, James Noble, Tobias Wrigstad, Springer-Verlag. LNCS 7850 319--365.
  • CS 115 Introduction to Computer Science
  • CS 182 Introduction to Computer Science Honors II
  • CS 496 Principles of Programming Languages
  • CS 510 Principles of Programming Languages
  • CS 643 Formal Verification of Software
  • CS 135 Discrete Structures
  • CS 485 Societal Impact of Information Technologies