Collaborative Research: FMitF: Track II: From Theory to Practice: Making Complex Invariants Accessible with DIG

Program invariants, which describe properties that always hold at a program location, are essential for program understanding, debugging, and verification. Among existing modern invariant learning work, the DIG tool can discover rich numerical invariants in programs by integrating dynamic inference and symbolic checking. However, while DIG has inspired many research projects and applications, it needs better scalability to support industry settings, and like other invariant research tools, it is generally not accessible to software developers and engineers who may lack the familiarity or time to learn its usage.

This project aims to develop DIG-I (DIG-Industry) to make DIG more practical and usable. The project's novelties are optimizations to improve DIG’s performance and scalability as well as integration with artificial intelligence (AI) to learn invariants more effectively. The project's impacts are that the open-source DIG-I tool will enhance the efficiency and usability of invariant learning, benefiting developers in industry and research labs, and will be used to introduce formal methods and invariant generation to students and professionals through courses at George Mason University.

This proposal will develop DIG-I to make invariant research more practical and accessible. It focuses on (i) improving performance by transforming expensive matrix and constraint-solving operations in DIG to Compute Unified Device Architecture (CUDA) kernels to be run efficiently on Graphics Processing Units (GPUs), (ii) supporting additional useful invariants and their applications by integrating existing invariant work directly into DIG's base code, (iii) modernizing DIG by adopting large language models (LLMs) to learn invariants more effectively, and (iv) improving the usability and adoption of invariant analysis by developing a Language Server Protocol (LSP) that allows invariant tools to integrate with popular Integrated Development Environments (IDEs) and editors such as Visual Studio (VS) Code.

The findings from this project will be used in the investigators’ courses, and mentoring and outreach activities.

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.