MURAL - Maynooth University Research Archive Library



    Evaluating the use of a general-purpose benchmark suite for domain-specific SMT-solving


    Healy, Andrew and Monahan, Rosemary and Power, James F. (2016) Evaluating the use of a general-purpose benchmark suite for domain-specific SMT-solving. In: SAC '16 Proceedings of the 31st Annual ACM Symposium on Applied Computing. ACM, pp. 1558-1561. ISBN 9781450337397

    [img]
    Preview
    Download (308kB) | Preview


    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...



    Add this article to your Mendeley library


    Abstract

    Benchmark suites are an important resource in validating performance requirements for software. However, generalpurpose suites may be unsuitable for domain-specific purposes, and may provide an incorrect indication of the software performance. This paper uses SMT-solvers (Satisfiability Modulo Theories) as a case-study. Taking deductive software verification as a specific application domain for SMT-solvers, we present an approach to quantifying the difference between generalpurpose and domain-specific benchmark suites. We show that workload-based clustering of benchmark programs increases the specificity of features tested by the suite compared to the inherent hierarchy of a general-purpose suite.

    Item Type: Book Section
    Keywords: Benchmarks; SMT solvers; software verification; profiling;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Item ID: 10223
    Identification Number: https://doi.org/10.1145/2851613.2851975
    Depositing User: Dr. James Power
    Date Deposited: 16 Nov 2018 15:15
    Publisher: ACM
    Refereed: Yes
    URI:
    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)

    View Item Item control page

    Downloads

    Downloads per month over past year

    Origin of downloads