Dave Naumann
Professor and Chair of the Department of Computer Science
Charles V. Schaefer, Jr. School of Engineering and Science
Department of Computer Science
Education
- PhD (1992) University of Texas at Austin (Computer Science)
- BA (1982) University of Texas at Austin (Computer Science)
Research
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.
Experience
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
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
Institutional Service
- Department Chair Chair
- CS Faculty Mentoring Committee Member
- CS Curriculum Committee Member
- Executive committee for promotion, tenure, reappointment Chair
- Tenure Track Search Committee Member
- CS Strategic Planning Committee Chair
- College of Online and Professional Education - Dean search committee Member
- Interim department chair Chair
- CS Chair Search Committee Chair
- Course transfer evaluator Chair
- Institute Promotion and Tenure Committee Member
- Review committee for reappointment of Dean Jean Zu Member
- Bloom Scholarship Selection Committee Chair
- miscellaneous activity Member
- Department self study committee Chair
- Tenured Promotion Workshop Member
- 150th Anniversary Academic Symposium Committee Member
- Miscellaneous activities Member
- SES Honors and Awards Committee Member
- Society of Computer Science (SOCS) Member
- School of Business P&T committee Member
Professional Service
- IEEE Computer Security Foundations Symposium Chair, Test of Time Award Committee
- ACM Transactions on Programming Languages and Systems Associate Editor
- Formal Aspects of Computing Member of editorial board
- ACM Nominated Jana Hofmann's dissertation for ACM award
- ACM SIGPLAN-M (Special interest group in programming languages, mentoring) Mentor
- Canadian National Science and Engineering Research Council Grant proposal reviewer
- Journal of Computer Security Guest editor
- Journal of Object Technology Member of editorial board
- Journal of Computer Security Guest editor
- NSF Proposal review panelist
- Symposium on Computer Security Foundations Member, Test of Time Award committee
- IEEE Symposium on Computer Security Foundations Program co-chair
- European Association for Computer Science and Logic Nominator, Ackermann Award
- INRIA France Evaluator for promotion of researcher
- Technical University of Darmstadt Evaluator of faculty candidates
- Workshop on Logics and Syntax of Low-level Languages Member of technical program committee
- IEEE Symposium on Computer Security Foundations Member of technical program committee
- INRIA (French research agency) Chair, Panel of Experts
- NSF Proposal reviewer
- ACM Symposium on Principles of Programming Languages (POPL) Member of technical program committee
- ACM workshop on Principles of Secure Compilation Member of technical program committee
- Brazilian Symposium on Formal Methods Member of technical program committee
Consulting Service
Microsoft Research
Vulcan Inc.
Galois Inc.
Vulcan Inc.
Galois Inc.
Appointments
Professor of Computer Science since 2008
Associate Professor of Computer Science 2002-08
Assistant Professor of Computer Science 1997-2002
Associate Professor of Computer Science 2002-08
Assistant Professor of Computer Science 1997-2002
Honors and 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.
Invited keynote speaker, Software Factory 4.0 annual meeting 2020.
Nominated for best paper, ETAPS 2023.
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.
Invited keynote speaker, Software Factory 4.0 annual meeting 2020.
Nominated for best paper, ETAPS 2023.
Professional Societies
- ACM – Association for Computing Machinery Member
- IEEE Member
- AAAS – American Association for the Advancement of Science Member
Grants, Contracts and 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.
Siemens Fellowship for High Assurance.
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.
Siemens Fellowship for High Assurance.
Patents and Inventions
Patent US 10,904,291 B1, Jan. 26, 2021: Low-overhead software transformation to enforce information security policies
Selected Publications
Book
- Naumann, D. A. (2022). Proceedings of IEEE Symposium on Computer Security Foundations (vol. 35). IEEE Press.
- Naumann, D.; Kuesters, R. (2021). Proceedings of IEEE Symposium on Computer Security Foundations (vol. 34). IEEE Press.
Book Chapter
- Naumann, D. A. (2022). Personal recollections of Edsger W. Dijkstra. Edsger Wybe Dijkstra: His Life, Work, and Legacy. Association for Computing Machinery.
Conference Proceeding
- Nagasamudram, R.; Beringer, L.; Birman, K.; Milano, M.; Naumann, D. A. (2024). Verifying a C implementation of Derecho's coordination mechanism using VST and Coq. Proceedings of 16th NASA International Formal Methods Symposium (pp. 99-117).
- Murray, T.; Tiwari, M.; Ernst, G.; Naumann, D. A. (2023). Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications. ACM Conference on Computer and Communications Security (pp. 1746-1760). ACM.
- Ramos, F.; Sabino, N.; Adão, P.; Naumann, D.; Santos, J. F. (2023). Toward Tool-Independent Summaries for Symbolic Execution. European Conference on Object-Oriented Programming (vol. 263, pp. 24:1-24:29).
- Nagasamudram, R.; Banerjee, A.; Naumann, D. A. (2023). The WhyRel Prototype for Modular Relational Verification of Pointer Programs. 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (vol. 13994 LNCS, pp. 133-151).
- Naumann, D. A.; Nagasamudram, R. (2021). Alignment Completeness for Relational Hoare Logics . Proceedings ACM/IEEE Symposium on Logic in Computer Science. ACM/IEEE Symposium on Logic in Computer Science (vol. 36).
- Ngo, M.; Naumann, D. A.; Rezk, T. (2020). Type-based relaxed noninterference for free. Proceedings, 22d International Conference on Formal Engineering Methods. IEEE.
- Appel, A. W.; Naumann, D. (2020). Verified sequential Malloc/Free. International Symposium on Memory Management (ISMM) (pp. 48--59). ACM.
https://doi.org/10.1145/3381898.3397211.
Journal Article
- Nagasamudram, R.; Koskinen, E.; Naumann, D. A. (2023). An algebra of alignment for relational verification. Proceedings of the ACM Programming Languages (POPL ed., vol. 7, pp. 574-603). ACM Press.
https://arxiv.org/abs/2202.04278. - Banerjee, A.; Nagasamudram, R.; Naumann, D. A.; Nikouei, M.. A Relational Program Logic with Data Abstraction and Dynamic Framing. ACM Transactions on Programming Languages and Systems . ACM.
Technical Report
- Nikouei, M.; Banerjee, A.; Naumann, D. (2019). Data Abstraction and Relational Program Logic. CoRR (vol. abs/1910.14560).
http://arxiv.org/abs/1910.14560.