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.