# Predicting SMT Solver Performance for Software Verification

## TL;DR

This paper introduces Where4, a machine learning-based portfolio system that predicts the most suitable SMT solver for software verification tasks in Why3, improving efficiency without requiring deep solver knowledge.

## Contribution

The paper presents a novel portfolio approach using static code metrics and machine learning to predict the best SMT solver for proof obligations in Why3.

## Key findings

- Improved proof success rate using the portfolio approach
- Reduced verification time compared to single solver use
- Seamless integration with existing Why3 infrastructure

## Abstract

The Why3 IDE and verification system facilitates the use of a wide range of Satisfiability Modulo Theories (SMT) solvers through a driver-based architecture. We present Where4: a portfolio-based approach to discharge Why3 proof obligations. We use data analysis and machine learning techniques on static metrics derived from program source code. Our approach benefits software engineers by providing a single utility to delegate proof obligations to the solvers most likely to return a useful result. It does this in a time-efficient way using existing Why3 and solver installations - without requiring low-level knowledge about SMT solver operation from the user.