| Autor: |
Andrew Healy, Rosemary Monahan, James F. Power |
| Jazyk: |
angličtina |
| Rok vydání: |
2017 |
| Předmět: |
|
| Zdroj: |
Electronic Proceedings in Theoretical Computer Science, Vol 240, Iss Proc. F-IDE 2016, Pp 20-37 (2017) |
| Druh dokumentu: |
article |
| ISSN: |
2075-2180 |
| DOI: |
10.4204/EPTCS.240.2 |
| Popis: |
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. |
| Databáze: |
Directory of Open Access Journals |
| Externí odkaz: |
|
