David Naumann is Helping Secure Software Reliability
Programming code is everywhere — from phone software updates to secure websites and the apps we rely on every day. Users simply trust these codes to work properly and protect their personal information. But developers can’t rely on faith alone. They need assurance — especially when working with complex, mission-critical systems — that codes perform exactly as intended, every time.
At Stevens Institute of Technology, Dave Naumann, professor and chair of the Department of Computer Science, and his team are addressing that challenge with WhyRel, a powerful new tool that elevates the code verification process.
A smarter way to verify software
While overall testing and code reviews remain integral to software development, they can miss both subtle and complex problems. Formal verification offers a much stronger level of confidence, and that’s where WhyRel shines.
This new tool uses mathematical reasoning to prove that a program operates as intended under all conditions. But it’s not enough to verify that a new version works. So instead of simply looking at a single version of a program, WhyRel performs what’s called relational verification to prove how the original and updated versions of a program behave in relation to each other. This is especially important to ensure consistency when updating software, optimizing code and ensuring that sensitive data remains secure.
WhyRel doesn’t just check outputs — it builds formal proofs that a program behaves as it should. It uses an approach called modular verification, which allows the system to break down a program into smaller components and prove properties about each one. Developers don’t need to construct every step of a proof manually. The user guides the tool by adding logical annotations to the code; then the tool performs the heavy mathematical reasoning in the background, automatically.
WhyRel is a research prototype. But this auto-active design — combining automation and human insight — has the potential to be both powerful and practical in supporting real-world applications.
Research recognition and national support
WhyRel debuted at the 2023 TACAS conference, one of the top events for software verification research. The paper — co-authored by Naumann; Ramana Nagasamudram ‘25; and Anindya Banerjee, professor at the IMDEA Software Institute in Spain — was nominated for a Best Paper Award. A more in-depth version of the research was published in April 2025 in the International Journal of Software Tools for Technology Transfer.
Since then, the project has received national support. A three-year, $588,000 grant from the National Science Foundation is now funding the next stage of development under the title “Auto-active Hyperproperty Verification for Security.” The grant supports ongoing theoretical work and is helping train the next generation of computer science researchers.
WhyRel reflects the university’s longstanding tradition of excellence in formal methods — the area of computer science that uses mathematics to verify software behavior. The Department of Computer Science is home to a growing group of researchers working at the intersection of programming languages, systems, cybersecurity and verification. That leadership is further underscored by the Bloom Chair in Computer Science, established in honor of the late Professor Stephen Bloom, whose pioneering work helped lay the foundations of modern verification methods.
Naumann sees WhyRel as a continuation of that legacy.
“Developers and users have to be able to trust that mission-critical code works in every situation,” Naumann said. “That’s why forward-thinking tools like WhyRel are so important. At Stevens, we’re proud to be pushing those boundaries.”
