Dr. Naumann’s research focus is on formal methods and software security, including: Java Modeling Language (JML); ad hoc network application security; fine-grained confidentiality/integrity policies; automated analysis/transformation of programs to enforce such policies; and methodology for formal specification of system components.
He is affiliated with CASSIA, the Center for the Advancement of Secure Systems and Information Assurance, whose mission is to foster collaboration and act as a catalyst for research, education, and entrepreneurship in information assurance and cybersecurity.
Dr. Naumann has projects supported through various funding sources, with research topics ranging from Java Modeling Language (JML), Access control and downgrading in information flow assurance, and high assurance for security in wireless networking. He co-chaired (with Stephen Chong) the 4th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security associated with PLDI 2009 in Dublin and co-chaired (with Peter O'Hearn) the 2008 Theory Workshop of the Second IFIP Working Conference on Verified Software: Theories, Tools, Experiments in Toronto. Also co-chair for 2010. He also chaired the Theory Panel of the Verified Software Initiative and am a Corresponding Member of the Verified Software Repository Network.
His work has resulted in honors including Best paper, ETAPS 2005, Davis Memorial Award for Research Excellence, 2006, Best student paper (coauthor), OOPSLA 2007, and Distinguished paper, ECOOP 2008.
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
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
David Naumann, Augusto Sampaio, and Leila Silva. ( 2012). Refactoring and Representation Independence for Class Hierarchies, Theoretical Computer Science, 433 60-97
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
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
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
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
Andrey Chudnov and David A Naumann. (Jun 2010). Information Flow Monitor Inlining, Computer Security Foundations Symposium. IEEE Press
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
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
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
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