We are thrilled to announce that Professor Weihao Qu was awarded an NSF CRII grant titled: Precise Formal Verification of General Relational Quantitative Properties with Mutable Arrays. The award is for nearly $180,000 for work over the next two years.
Project Summary: Modern software systems often juggle sensitive data, user privacy, and efficiency, all while navigating complex real-world scenarios. To ensure these qualities, researchers rely on relational reasoning, analyzing how a program behaves with different inputs or under varying conditions. While this approach is powerful, current tools often fall short when it comes to handling features like mutable arrays, a key data structure in many practical applications.
This groundbreaking project introduces a new formal verification framework designed to overcome these challenges, enabling precise and general analysis of programs that use mutable arrays. By employing fine-grained techniques, the framework captures the behavior of individual array elements instead of treating arrays as a whole. This approach leads to significantly more detailed and accurate verification results.
The research also pushes the boundaries of relational reasoning by generalizing existing methods to support a wider range of relational quantitative properties. These advancements will be integrated into a unified framework, blending theoretical breakthroughs with practical tools, and rigorously evaluated on real-world software. By addressing critical gaps in precision and applicability, this work has the potential to reshape how we understand and verify software, paving the way for systems that are more secure, private, and efficient. This project not only bridges theoretical and practical divides but also sets a new standard for software correctness and reliability in an increasingly data-driven world.