Predicting SMT Solver Performance for Software Verification

Andrew Healy
(Maynooth University)
Rosemary Monahan
(Maynooth University)
James F. Power
(Maynooth University)

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.

In Catherine Dubois, Paolo Masci and Dominique Méry: Proceedings of the Third Workshop on Formal Integrated Development Environment (F-IDE 2016), Limassol, Cyprus, November 8, 2016, Electronic Proceedings in Theoretical Computer Science 240, pp. 20–37.
Published: 27th January 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: