CAREER: Computing Program Invariants using Abstract Domains Search

Computer software has become embedded in the very fabric of how society works and plays. However, as software continues to increase in size and complexity, program analysts and software engineers find it increasingly challenging to keep computer software secure, reliable, and safe. To do so, they use what is called software verification. Program invariants are an essential part of software verification; they are summaries of possible program behaviors. Unfortunately, current methods for computing program invariants are not keeping pace with software complexity, resulting in approaches that do not scale well, or which compute imprecise, i.e., weak program invariants. In addition, while better strategies for developing program invariants are available, they are too difficult for most engineers to apply without highly specialized training. This project will produce novel techniques to overcome these limitations to compute strong program invariants, and to do so far more easily. Since program invariants touch on so many parts of software engineering such as generating, debugging, verifying, and optimizing computer code, improved accuracy and efficiency can transform software development. In addition, the investigator at Boise State University in Boise, Idaho will work closely with regional industry professionals both to enhance their verification training, as well as to collaborate in co-developing a graduate-level class on applied program analysis.

The project will use an approach for computing program invariants called abstract interpretation. Key to effective abstract interpretation is choosing an appropriate abstraction level for static code analysis. On the one hand, if the abstraction is too fine, it will not scale well. On the other hand, if the abstraction is too coarse, it will compute weak invariants. This project will result in a novel approach for finding suitable abstractions that allows for a scalable, precise, and far more accessible method of computing program invariants. The resulting Search-based Static Analysis (SBSA) framework will significantly improve upon current static analysis methods and use search techniques to automatically optimize abstract interpreter configurations. It will also facilitate new research directions that require strong program invariants. There are three project objectives, to: (1) investigate search techniques to find the best abstract domain, (2) explore mechanisms for guiding the abstract domain search based on software concrete semantics, and (3) improve precision by strategically partitioning software into components and then analyzing them separately to enable better search.

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.