Dave Naumann
| Professor and Department Chair of Computer Science |
| Stevens Institute of Technology |
| Hoboken, NJ, USA |
| Contact and CV |
Table of Contents
Research
My focus is on formal methods and software security, including: relational and hyperproperty verification; fine-grained confidentiality/integrity policies; program analysis, verification, and transformation; correctness by construction; program logics and machine-checked metatheory; and methodology for formal specification of distributed system components.
I'm in the Cypress group.
Publications
Some recent papers:
Forall-Exists Relational Verification by Filtering to Forall-Forall (with Ramana Nagasamudram and Anindya Banerjee) 2025.
Alignment complete relational Hoare logics for some and all (with Ramana Nagasamudram and Anindya Banerjee) 2025.
The WhyRel Prototype for Modular Relational Verification of Pointer Programs (with Ramana Nagasamudram and Anindya Banerjee) in TACAS 2023. Extended version WhyRel: an Auto-active Relational Verifier in Software Tools for Technology Transfer 2025.
Verifying a C implementation of Derecho's coordination mechanism using VST and Coq (with Ramana Nagasamudram, Lennart Beringer, Ken Birman, and Mae Milano) in NASA Formal Methods Symposium 2024.
An Algebra of Alignment for Relational Verification (with Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram and Minh Ngo) in POPL 2023.
Toward Tool-Independent Summaries for Symbolic Execution (with Frederico Ramos, Nuno Sabino, Pedro Adão and José Fragoso Santos) in ECOOP 2023.
Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (with Toby Murray, Mukesh Tiwari and Gidon Ernst) in CCS 2023.
A Relational Program Logic with Data Abstraction and Dynamic Framing (with Anindya Banerjee, Ramana Nagasamudram, and Mohammad Nikouei) in ACM TOPLAS 2022.
Advisees
Current and past PhD students: Jude Kanjamala; Ramana Nagasamudram (defended 2025); Mohammad Nikouei (defended 2019); Andrey Chudnov (defended 2016); Chunyu Tang (defended 2013); Stan Rosenberg (defended 2011); Qi Sun (defended 2007).
Postdoctoral research associates: Minh Ngo (2019), Mounir Assaf (2015–17).
Support
Siemens, Microsoft Research, NSF CNS-2426414, NSF CNS-1718713, NSF CCF-1649884, NSF DeepSpec
Teaching
Courses
Fall 2024: CS 643 Formal Verification of Software
Assistantships
Undergraduate summer research: Contact me early in Spring semester for projects.
PhD positions: From time to time I take on new PhD students for research on software verification and secure information flow: policies, static analysis, and runtime monitoring. Full funding is provided. The ideal candidates have background in programming language theory and implementation or formal methods.
Recent service
Program committee co-chair, IEEE Computer Security Foundations Symposium (2021 and 2022)
Program committee member: ACM Principles of Programming Languages (2023, 2019), ACM Computer and Communication Security (2025), IEEE Computer Security Foundations (2025), European Conference on Object-Oriented Programming (2024)
Editorial boards: ACM Transactions on Programming Languages and Systems, Formal Aspects of Computing, Journal of Object Technology
Miscellany
A series of noun phrases (lacunae not shown)
Mentoring for PL research; Childhood beyond brands; Verifying what counts; my Chinese name (那 德 维); where my page should be; Capoeira Angola Center of Mestre João Grande; Freedom to Tinker; Smyrneika, guitar, and voice teachers; speed limits for chumps; African diaspora; timeliness of my stylish home page; the cry of the imaginary cuica.