EAGER: CCF: SHF: Scalable Software Verification through Automated Derivation of Domain-Specific Optimization Tactics

The ever-growing reliance of society on software-intensive systems drives a continued demand for increased software dependability, making it more important than ever. Formal-verification techniques provide the highest degree of software assurance, with their strengths residing in their automated yet rigorous analysis capabilities. Performing such formal analyses is, however, an expensive endeavor, facing scalability issues.

This challenge is exacerbated when considering the evolving nature of complex systems. The high cost of formal verification is thus prohibitive for rapidly evolving large-scale systems, despite the benefits it can offer for reliability, safety, and security. This research seeks to develop techniques for automating the development of optimizations for software-verification techniques with the aim that each system of interest can have verification tailored to its specific characteristics, thereby significantly reducing the verification cost.

This, in turn, allows software engineers to continuously analyze evolving systems online, rather than the current practice of performing expensive, long-running formal analysis once, if at all, during the entire development process. In addition to graduate students, this project will attempt to involve undergraduate, female, and underrepresented minority students.

This research project explores the possibility of driving the automated discovery of domain-specific optimizations for software-verification techniques. Historically, such optimizations have arisen from the insights of a few dozen experts in software verification worldwide. This research is taking a different approach.

The project seeks to automatically infer domain-specific, sound optimizations to trim the verification bounds without requiring any prior domain expertise on the part of the analyzer, promising to make software verification significantly more scalable and cost-effective. The intellectual merit of this research is a novel, speculative analysis, underpinned by established, proven model-finding technologies to automatically recognize opportunities for the derivation of sound optimizations, without requiring domain expertise or excessive overhead, thereby significantly diminishing the analysis cost.

This research promises to advance the state-of-the-art by rendering bounded formal verification more tractable, thereby expanding the areas that can practically benefit from formal verification techniques.

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.