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
JP-Predicting-2016.pdf
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: | |
| URI: | https://mural.maynoothuniversity.ie/id/eprint/8217 |
| 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
Downloads per month over past year
