CIS Seminar Series 2026 -David Naumann Ph.D.-Stevens Institute of Technology

Relational verification: recent results and open problems

ABSTRACT

Relational verification encompasses reasoning about data abstraction, information flow security and privacy, correct compilation, validation of code revisions, and other applications. This talk will introduce relational properties especially the important classes of $\forall\forall$ and $\forall\exists$ properties. Verification techniques will be outlined, including product automata, product programs, alignment, program rewriting, and relational Hoare logics. A novel transformation will be shown, which reduces $\forall\exists$ verification to $\forall\forall$. The transformation has been validated through experiments using a prototype tool and through machine-checked proof. The talk will conclude with current research challenges.

BIOGRAPHY

David Naumann Professor of Computer Science and Associate Dean for Research and Faculty Development in the School of Computing at Stevens Institute of Technology His current research interests include specification and verification of information flow security using deductive systems, static analyses, and runtime monitoring, as well as epistemic reasoning in distributed system design and verification. His work has been supported by the National Science Foundation, Department of Homeland Security, the Swedish Emergency Management Agency, Siemens Corp., Microsoft, SRI International, Vulcan Inc., and Galois Inc. He has held visiting positions at Microsoft Research (Cambridge UK), IMDEA Software (Madrid), Princeton University, and (currently) Cornell University.