Their project addresses a fundamental challenge in software engineering: ensuring that code behaves correctly under all conditions. Software systems are conventionally validated using unit testing, which confirms that the system behaves properly on particularly chosen input/output pairs. While efficient, this technique may miss defects exposed by other inputs. A longstanding alternative is called formal verification, which provides a mathematically rigorous approach to validating software behavior. However, this technique is difficult to apply to large, real-world systems due to its complexity and high cost. Amusuo and Anandayuvaraj aim to change that.

 

Their research focuses on a promising approach to formal verification known as unit proofing—a process similar to unit testing that involves breaking down software into smaller, verifiable components and proving the correctness of each piece individually. This modular approach makes formal verification more accessible and practical for developers.

 

Through an extensive study of unit proofing practices at major organizations such as Amazon Web Services, Amusuo and Anandayuvaraj identified key shortcomings in current methods, including their manual nature, inconsistency, and susceptibility to error. In some cases, flawed unit proofs not only fail to catch bugs but also obscure critical vulnerabilities.

 

To address these issues, they developed a new framework that streamlines the creation and maintenance of unit proofs. They applied the method manually and demonstrated a 16-fold improvement in verification efficiency and has led to the discovery of 20 previously unknown, or “zero-day,” security vulnerabilities. Amusuo says code-level defects like buffer overflows remain a major concern in software development. He says formal verification offers strong guarantees against such bugs, but it's often too costly and difficult to adopt.

 

“I am excited about the potentials of our proposal to make formal verification more accessible --- through systematic guidance and automated tooling,” says Amusuo. “When completed, our goal is to enable engineers to verify critical software components and eliminate these code-level defects before the software is deployed.”

 

Amusuo says the Qualcomm Innovation Fellowship is a strong validation of this work. He looks forward to collaborating with Qualcomm to build tools that bring formal verification into everyday engineering workflows.

 

Building on this work, Amusuo and Anandayuvaraj are now developing a suite of tools to automate parts of this task and support software engineers throughout the unit proofing process. These tools aim to automate key tasks such as decomposing code into verifiable units, generating and repairing unit proofs, and keeping them up to date as software evolves. They also exploring how program analysis techniques and large language models—like those used in tools such as ChatGPT—can further automate and enhance the process. Their partnership brings together their synergistic expertise in both aspects of the problem domain: Amusuo is an expert in program analysis and formal methods, and Anandayuvaraj is an expert in applying large language models to automate engineering tasks.

 

The vision is to make formal software verification as routine and affordable as traditional testing methods, enabling developers to identify and fix bugs earlier in the development cycle. If widely adopted, this approach could significantly improve software reliability and security across a range of applications.

 

The Qualcomm fellowship recognizes top graduate students who demonstrate exceptional technical talent and the potential to drive future innovation in the tech industry. Amusuo and Anandayuvaraj’s work exemplifies this potential, contributing to the future of safer and more dependable software systems.