Predicting SMT Solver Performance for Software Verification
This work addresses the challenge for software engineers in automating solver selection in verification tools, though it is incremental as it builds on existing Why3 infrastructure.
The paper tackles the problem of efficiently selecting SMT solvers for software verification by introducing Where4, a portfolio-based approach that uses static code metrics and machine learning to predict solver performance, resulting in improved time efficiency without requiring user expertise in solver operation.
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.