David A. Naumann

Professor of Computer Science at Stevens Institute of Technology. Here's contact info and Curriculum Vitae.

Publications etc.

Fall 2020 -- Introduction to Computer Science; and Formal Verification of Software

Spring 2020 -- Introduction to Computer Science

Fall 2019 -- Introduction to Computer Science; and Formal Verification of Software

Spring 2019 -- Formal Modeling and Analysis for Software Security

Fall 2018 -- Introduction to Computer Science; and Formal Verification of Software

Fall 2017 -- on sabbatical as Visiting Fellow at Princeton University, in the DeepSpec Expedition.

Spring 2017 -- Introduction to Computer Science Honors II

Fall 2016 -- Formal Modeling and Analysis for Software Security; and Societal Impact of Information Technologies


For undergrad and MS students: Scholarships for Service.

Undergraduate summer research: Contact me early in Spring semester for projects, supported by NSF and the Stevens Scholars program.

PhD positions: From time to time I take on new PhD students for research on secure information flow in software: policies, static analysis, and runtime monitoring for Android and other platforms. Full funding is provided. The ideal candidates have background in programming language theory and implementation or formal methods.


My focus is on formal methods and software security, including: ad hoc network application security; JavaScript and web security; fine-grained confidentiality/integrity policies; program analysis, verification, and transformation; correctness by construction; and methodology for formal specification of system components. For details see publications and tools.

Affiliated with: CASSIA, the Center for the Advancement of Secure Systems and Information Assurance; also the DeepSpec Expedition.

Postdoctoral research associates: Minh Ngo (2019) working on Relational Verification for Information Assurance and Privacy, NSF award SaTC CNS-1718713.
Mounir Assaf (2015-17) working on Hyperproperty Abstraction for Information Flow Control funded by NSF EAGER award CCF-1649884.

Current and past PhD students: Ramana Nagasamudram; Mohammad Nikouei (finished Fall 2019); Andrey Chudnov (finished Spring 2016); Chunyu Tang (finished Fall 2013); Stan Rosenberg (finished Summer 2011); Qi Sun (finished Fall 2007).

I'm working on Relational Verification for Information Assurance and Privacy (NSF award SaTC CNS-1718713).

I worked with Anindya Banerjee (IMDEA Software), Gary Leavens (U. Central FL.), and others on Flexible and Practical Information Flow Assurance for Mobile Apps (NSF award 1228930) --see the FlowSpecs project.
With support from DHS I worked on Tunable Information Flow with researchers at HRL Laboratories.
I work with Gary Leavens and others on the Java Modeling Language (JML), and with Leila Silva (UFS Brazil), Giovanny Lucero (UFS Brazil), and Augusto Sampaio (UFPE Brazil) on refactoring (NSF awards CNS-0708330 and CCF-0915611).
With support from Microsoft Research I worked with Andy Gordon and François Dupressoir on verifying cryptographic code in C, and collaborated on the Spec#/Boogie software specification/verification project.
With support from NSF I worked with Anindya Banerjee on Access Control and Downgrading in Information Flow Assurance, collaborating with Tamara Rezk and Gilles Barthe (INRIA), Marco Pistoia (IBM), Qi Sun and Stan Rosenberg. See our Secure Information Flow Inferencer and Verifier for Region Logic.
With support from Telcordia and the U.S. Government I worked with Susanne Wetzel and Chunyu Tang on high assurance for security in wireless networking.

Selected recent program committees and editorial boards
IEEE Symposium on Computer Security Foundations (CSF) 2021 (co-chair), 2020, 2019, 2015
24th International Symposium on Formal Methods (FM) 2021
28th European Symposium on Programming (ESOP) 2019
ACM SIGPLAN Symposium on Principles of Programming Languages (POPL) 2019, 2011
Syntax and Semantics of Low-Level Languages (LOLA) 2018
2nd Workshop on Principles of Secure Compilation (PriSC) 2018
International Conference on Runtime Verification, 2014, 2016
20th International Symposium on Formal Methods (FM) 2015
4th Conference on Principles of Security and Trust (POST) 2015
5th International Symposium on Unifying Theories of Programming (UTP) 2014 (PC chair)
Programming Languages and Analysis for Security (PLAS) 2014, 2009 (co-chair), 2008
Workshop on Foundations of Computer Security (FCS) at LICS/CSF 2013
Verified Software: Theories, Tools, Experiments 2008, 2010, & 2013
1st ACM Workshop on Higher-Order Programming with Effects (HOPE) at ICFP 2012
ACM Conference on Computer and Communication Security (CCS) 2010
ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP) 2013
New Jersey Programming Languages Seminar (NJPLS) co-organizer, April 2010.
International Conference on Formal Engineering Methods (ICFEM) 2009.
Brazilian Symposium on Formal Methods (SBMF) 2007-2015 (also Steering Committee, and co-chair of PC 2012)
Mathemetics of Program Construction 2004, 2010, 2012

I co-chaired (with Rohit Gheyi) the 15th Brazilian Symposium on Formal Methods. I co-chaired (with Stephen Chong) the 4th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security associated with PLDI 2009 in Dublin. I co-chaired (with Peter O'Hearn) the 2008 Theory Workshop of the Second IFIP Working Conference on Verified Software: Theories, Tools, Experiments and I co-chaired the Theory Workshop for 2010. I chaired the Theory Panel of the Verified Software Initiative and am a Corresponding Member of the Verified Software Repository Network.

Editorial Boards: ACM Transactions on Programming Languages and Systems (TOPLAS), Formal Aspects of Computing, and The Journal of Object Technology.

A series of noun phrases (lacunae not shown)

The timeliness of my stylish home page, Freedom to Tinker, Empowering Underrepresented Groups in Technology, speed limits for chumps, my guitar teacher, verifying what counts, air quality, life above 20 kHz, my Capoeira Angola master, quanta, the African diaspora, my Smyrneika and voice teachers shaking away like a rattlesnake, pop record ageing fan, Pandora's locked box, the desk upon which it stands, the cry of the imaginary cuica.