# Predicting SMT Solver Performance for Software Verification

arXiv: https://arxiv.org/abs/1701.08466 · HTML: https://mlsanity.com/paper/1701.08466/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Jan 2017.

## Built on by (most cited first, 1 of 1)

- [Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis](https://mlsanity.com/paper/2307.09564/) (2023)

## Abstract (arXiv)

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.