Healy, Andrew and Monahan, Rosemary and Power, James F. (2016) Predicting SMT Solver Performance for Software Verification. Working Paper. arXiv.

Preview

Download (357kB) | Preview

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.

Item Type:	Monograph (Working Paper)
Additional Information:	Cite as: arXiv:1701.08466 [cs.SE]. This work is licensed under the Creative Commons Attribution License. In 3rd Workshop on Formal Integrated Development Environment, volume 240 of Electronic Proceedings in Theoretical Computer Science, pages 20--37, Limassol, Cyprus, November 8 2016.
Keywords:	SMT Solver Performance; Software Verification; Why3 IDE; verification system; Satisfiability Modulo Theories (SMT);
Academic Unit:	Faculty of Science and Engineering > Computer Science
Item ID:	8217
Identification Number:	https://doi.org/10.4204/EPTCS.240.2
Depositing User:	Dr. James Power
Date Deposited:	17 May 2017 15:39
Publisher:	arXiv
URI:	https://arxiv.org/
Use Licence:	This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

Repository Staff Only(login required)

Item control page

Downloads

Origin of downloads