CRII:SHF: Precise Formal Verification of General Relational Quantitative Properties with Mutable Arrays

Software systems often need to handle sensitive data securely, maintain user privacy, and operate efficiently. One way to ensure these qualities is by analyzing how a program behaves when it processes different inputs or runs in different situations. This type of analysis, called relational reasoning, helps uncover important properties like whether a program protects sensitive information or performs tasks consistently.

While tools exist for analyzing some programs, they often struggle to handle features like mutable arrays, which are widely used to store and manage data in practical applications. The project’s novelties are creating better tools to analyze programs that use arrays, making the process more precise and broadly applicable. By addressing key challenges in existing techniques, the research aims to bridge gaps in both theoretical understanding and practical implementation.

The project’s impacts are improving how we understand and verify programs, and helping create software that is more secure, private, and efficient. The project will provide training in formal verification research for undergraduate and graduate students. The results from the research will be incorporated into university courses taught by the lead investigator.

This project introduces a formal verification framework to enable precise and general reasoning about relational quantitative properties in programs with mutable arrays. To address the challenge of imprecision, the investigator will leverage fine-grained analysis techniques that capture the behavior of individual array elements rather than treating the entire array as a single unit.

This allows for more detailed and accurate verification results. To expand the scope of relational reasoning, the investigator will generalize existing techniques to support a broader range of relational quantitative properties involving mutable arrays, including those beyond current limitations. The research will integrate these advances into a unified framework, combining theoretical insights with practical tool development, and evaluate the system on real-world software.

This work is expected to significantly advance the field of relational quantitative reasoning by addressing critical gaps in precision and applicability, leading to better tools for ensuring software correctness and reliability.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.