MURAL - Maynooth University Research Archive Library



    Predicting SMT Solver Performance for Software Verification


    Healy, Andrew and Monahan, Rosemary and Power, James F. (2017) Predicting SMT Solver Performance for Software Verification. Electronic Proceedings in Theoretical Computer Science, 240. pp. 20-37. ISSN 2075-2180

    [img]
    Preview
    Download (344kB) | Preview


    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...



    Add this article to your Mendeley library


    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: Article
    Keywords: Why3; Satisfiability ModuloTheories (SMT); Where4;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Faculty of Science and Engineering > Research Institutes > Hamilton Institute
    Item ID: 11670
    Identification Number: https://doi.org/10.4204/EPTCS.240.2
    Depositing User: Rosemary Monahan
    Date Deposited: 12 Nov 2019 12:37
    Journal or Publication Title: Electronic Proceedings in Theoretical Computer Science
    Publisher: Open Publishing Association
    Refereed: Yes
    URI:

    Repository Staff Only(login required)

    View Item Item control page

    Downloads

    Downloads per month over past year