Verification Coverage
This addresses a specific obstacle for broader adoption of formal verification tools in software engineering, but it is an incremental adaptation of existing coverage concepts to a new context.
The paper tackles the problem that software model checkers often fail to provide progress measures when they cannot fully analyze instances within resource limits, by proposing a verification coverage metric inspired by test coverage for Abstract Reachability Tree-based techniques. They develop a method to compute an under-approximation of this metric and show through empirical evaluation that it is viable, though no concrete performance numbers are provided.
Software Model Checkers have shown outstanding performance improvements in recent times. Moreover, for specific use cases, formal verification techniques have shown to be highly effective, leading to a number of high-profile success stories. However, widespread adoption remains unlikely in the short term and one of the remaining obstacles in that direction is the vast number of instances which software model checkers cannot fully analyze within reasonable memory and CPU bounds. The majority of verification tools fail to provide a measure of progress or any intermediate verification result when such situations occur. Inspired in the success that coverage metrics have achieved in industry, we propose to adapt the definition of coverage to the context of verification. We discuss some of the challenges in pinning down a definition that resembles the deeply rooted semantics of test coverage. Subsequently we propose a definition for a broad family of verification techniques: those based on Abstract Reachability Trees. Moreover, we discuss a general approach to computing an under-approximation of such metric and a specific heuristic to improve the performance. Finally, we conduct an empirical evaluation to assess the viability of our approach.