Share and Export
Share and Export
Healy, Andrew, Monahan, Rosemary and Power, James F. (2016) Predicting SMT Solver Performance for Software Verification. Working Paper. arXiv.
Preview
Available under License Creative Commons Attribution Non-commercial Share Alike.
Download (357kB) | Preview
Official URL: https://arxiv.org/abs/1701.08466
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: | 10.4204/EPTCS.240.2 |
| Depositing User: | Dr. James Power |
| Date Deposited: | 17 May 2017 15:39 |
| Publisher: | arXiv |
| Related URLs: | |
| 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 |
Downloads
Downloads per month over past year
Origin of downloads
Altmetric Badge
Repository Staff Only (login required)
- Item control page
