Predicting SMT Solver Performance for Software Verification
Software Engineering
2017-01-31 v1 Machine Learning
Logic in Computer Science
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.
Cite
@article{arxiv.1701.08466,
title = {Predicting SMT Solver Performance for Software Verification},
author = {Andrew Healy and Rosemary Monahan and James F. Power},
journal= {arXiv preprint arXiv:1701.08466},
year = {2017}
}
Comments
In Proceedings F-IDE 2016, arXiv:1701.07925