Collaborative Research: FMitF: Track II: Enabling Pluggable Runtime Verification Optimizations

Lightweight formal methods offer a way to increase the use of rigorous techniques for finding more bugs during everyday software development. Runtime verification (RV) is such a method; it monitors program executions against behavioral safety properties that are specified in logic. In many open-source projects, RV has helped find hundreds of confirmed bugs that were missed during software testing; but RV is often too slow. While several optimizations have been proposed for speeding up RV, no extant framework implements all of them. The project’s novelties are a framework for implementing RV optimizations and re-implementations of existing optimizations in that framework. The project’s impacts are faster RV during software testing and a platform for investigating future optimizations.

The project will (i) develop a framework for making optimizations pluggable into implementations of popular but often slow-for-testing RV tools; (ii) re-engineer two existing RV tools to accommodate that framework; and (iii) re-implement two existing optimizations within that framework. The investigators plan to evaluate the proposed framework by (i) comparing their framework-enhanced tools with state-of-the-art tools that do not implement said optimizations, and by (ii) assessing the ease with which a third optimization can be plugged into the framework. The investigators will use their existing RV tools and their benchmarks of formal specifications and actively develop open-source projects for this evaluation.

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.

Award Number: 2525242
Principal Investigator: Rahul Purandare
Funds Obligated: $75,000
State: NE