Share and Export
Share and Export
Healy, Andrew, 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
Preview
Available under License Creative Commons Attribution Non-commercial Share Alike.
Download (308kB) | Preview
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: | 10.1145/2851613.2851975 |
| Depositing User: | Dr. James Power |
| Date Deposited: | 16 Nov 2018 15:15 |
| Publisher: | ACM |
| Refereed: | Yes |
| Related URLs: | |
| 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 |
Downloads
Downloads per month over past year
Origin of downloads
Altmetric Badge
Repository Staff Only (login required)
- Item control page
