Empirical software metrics for benchmarking of verification tools

Area of Science:

• Computer Science
• Software Engineering
• Artificial Intelligence

Background:

• Software verification tools face challenges in predicting performance across diverse software types.
• Existing metrics may not fully capture the complexities influencing verification tool efficacy.

Purpose of the Study:

• To develop empirical software metrics capable of predicting verification tool performance.
• To construct a machine learning-based portfolio solver utilizing these novel metrics.
• To evaluate the solver's performance in the international Software Verification Competition (SV-COMP).

Main Methods:

• Extraction of software metrics including variable usage, loop patterns, and control-flow complexity via data-flow analysis.
• Development of a machine learning model to construct a portfolio solver based on extracted metrics.
• Evaluation of the portfolio solver's hypothetical performance against SV-COMP benchmarks from 2014-2016.

Main Results:

• The developed empirical metrics demonstrated strong predictive power for software verification tool performance.
• The machine learning-based portfolio solver hypothetically achieved top performance in SV-COMP for three consecutive years (2014-2016).
• The portfolio construction algorithm proved flexible and effective across different SV-COMP versions with varying tasks and tools.

Conclusions:

• Empirical software metrics derived from data-flow analysis are effective predictors of verification tool performance.
• Machine learning-based portfolio solvers represent a viable and high-performing approach to automated software verification.
• The proposed methodology offers a robust and adaptable framework for enhancing software verification strategies.