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

    Download (308kB) | Preview

    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...

    Add this article to your Mendeley library


    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:
    Depositing User: Dr. James Power
    Date Deposited: 16 Nov 2018 15:15
    Publisher: ACM
    Refereed: Yes
    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 per month over past year

    Origin of downloads