Skeletal approximation enumeration for SMT solver testing

Peisen Yao; Heqing Huang; Wensheng Tang; Qingkai Shi; Rongxin Wu; Charles Zhang

doi:10.1145/3468264.3468540

Skeletal approximation enumeration for SMT solver testing

Peisen Yao
, Heqing Huang^*
, Wensheng Tang
, Qingkai Shi
, Rongxin Wu
, Charles Zhang

^*Corresponding author for this work

Research output: Chapters, Conference Papers, Creative and Literary Works › RGC 32 - Refereed conference paper (with host publication) › peer-review

18 Citations (Scopus)

Abstract

Ensuring the equality of SMT solvers is critical due to its broad spectrum of applications in academia and industry, such as symbolic execution and program verification. Existing approaches to testing SMT solvers are either too costly or find difficulties generalizing to different solvers and theories, due to the test oracle problem. To complement existing approaches and overcome their weaknesses, this paper introduces skeletal approximation enumeration (SAE), a novel lightweight and general testing technique for all first-order theories. To demonstrate its practical utility, we have applied the SAE technique to test Z3 and CVC4, two comprehensively tested, state-of-the-art SMT solvers. By the time of writing, our approach had found 71 confirmed bugs in Z3 and CVC4,55 of which had already been fixed. © 2021 ACM.

Original language	English
Title of host publication	ESEC/FSE 2021
Subtitle of host publication	Proceedings of the 29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering
Publisher	Association for Computing Machinery
Pages	1141-1153
ISBN (Print)	978-1-4503-8562-6
DOIs	https://doi.org/10.1145/3468264.3468540
Publication status	Published - Aug 2021
Externally published	Yes
Event	29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2021 - Virtual, Online, Greece Duration: 23 Aug 2021 → 28 Aug 2021

Conference

Conference	29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2021
Place	Greece
City	Virtual, Online
Period	23/08/21 → 28/08/21

Funding

We thank the anonymous reviewers for their insightful comments. We also appreciate the developers of Z3 and CVC4 for discussing and addressing our bug reports. Rongxin Wu is supported by the Leading-edge Technology Program of Jiangsu Natural Science Foundation (BK20202001) and NSFC61902329. Other authors are supported by the RGC16206517 and ITS/440/18FP grants from the Hong Kong Research Grant Council, Ant Group through ant Research Program, and the donations from Microsoft and Huawei. Heqing Huang is the corresponding author.

Research Keywords

metamorphic testing
mutation-based testing
SMT solver testing

RGC Funding Information

RGC-funded

Access Output

10.1145/3468264.3468540

Other Access Options

Check CityUHK Library

Permanent Link

Right click to copy link

Cite this

Yao, P., Huang, H., Tang, W., Shi, Q., Wu, R., & Zhang, C. (2021). Skeletal approximation enumeration for SMT solver testing. In ESEC/FSE 2021 : Proceedings of the 29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering (pp. 1141-1153). Association for Computing Machinery. https://doi.org/10.1145/3468264.3468540

@inproceedings{767b16d8c1414ef59d27cd161932c5dc,

title = "Skeletal approximation enumeration for SMT solver testing",

abstract = "Ensuring the equality of SMT solvers is critical due to its broad spectrum of applications in academia and industry, such as symbolic execution and program verification. Existing approaches to testing SMT solvers are either too costly or find difficulties generalizing to different solvers and theories, due to the test oracle problem. To complement existing approaches and overcome their weaknesses, this paper introduces skeletal approximation enumeration (SAE), a novel lightweight and general testing technique for all first-order theories. To demonstrate its practical utility, we have applied the SAE technique to test Z3 and CVC4, two comprehensively tested, state-of-the-art SMT solvers. By the time of writing, our approach had found 71 confirmed bugs in Z3 and CVC4,55 of which had already been fixed. {\textcopyright} 2021 ACM.",

keywords = "metamorphic testing, mutation-based testing, SMT solver testing",

author = "Peisen Yao and Heqing Huang and Wensheng Tang and Qingkai Shi and Rongxin Wu and Charles Zhang",

year = "2021",

month = aug,

doi = "10.1145/3468264.3468540",

language = "English",

isbn = "978-1-4503-8562-6",

pages = "1141--1153",

booktitle = "ESEC/FSE 2021",

publisher = "Association for Computing Machinery",

address = "United States",

note = "29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2021 ; Conference date: 23-08-2021 Through 28-08-2021",

}

Yao, P, Huang, H, Tang, W, Shi, Q, Wu, R & Zhang, C 2021, Skeletal approximation enumeration for SMT solver testing. in ESEC/FSE 2021 : Proceedings of the 29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering. Association for Computing Machinery, pp. 1141-1153, 29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2021, Virtual, Online, Greece, 23/08/21. https://doi.org/10.1145/3468264.3468540

Skeletal approximation enumeration for SMT solver testing. / Yao, Peisen; Huang, Heqing; Tang, Wensheng et al.
ESEC/FSE 2021 : Proceedings of the 29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering. Association for Computing Machinery, 2021. p. 1141-1153.

Research output: Chapters, Conference Papers, Creative and Literary Works › RGC 32 - Refereed conference paper (with host publication) › peer-review

TY - GEN

T1 - Skeletal approximation enumeration for SMT solver testing

AU - Yao, Peisen

AU - Huang, Heqing

AU - Tang, Wensheng

AU - Shi, Qingkai

AU - Wu, Rongxin

AU - Zhang, Charles

PY - 2021/8

Y1 - 2021/8

N2 - Ensuring the equality of SMT solvers is critical due to its broad spectrum of applications in academia and industry, such as symbolic execution and program verification. Existing approaches to testing SMT solvers are either too costly or find difficulties generalizing to different solvers and theories, due to the test oracle problem. To complement existing approaches and overcome their weaknesses, this paper introduces skeletal approximation enumeration (SAE), a novel lightweight and general testing technique for all first-order theories. To demonstrate its practical utility, we have applied the SAE technique to test Z3 and CVC4, two comprehensively tested, state-of-the-art SMT solvers. By the time of writing, our approach had found 71 confirmed bugs in Z3 and CVC4,55 of which had already been fixed. © 2021 ACM.

AB - Ensuring the equality of SMT solvers is critical due to its broad spectrum of applications in academia and industry, such as symbolic execution and program verification. Existing approaches to testing SMT solvers are either too costly or find difficulties generalizing to different solvers and theories, due to the test oracle problem. To complement existing approaches and overcome their weaknesses, this paper introduces skeletal approximation enumeration (SAE), a novel lightweight and general testing technique for all first-order theories. To demonstrate its practical utility, we have applied the SAE technique to test Z3 and CVC4, two comprehensively tested, state-of-the-art SMT solvers. By the time of writing, our approach had found 71 confirmed bugs in Z3 and CVC4,55 of which had already been fixed. © 2021 ACM.

KW - metamorphic testing

KW - mutation-based testing

KW - SMT solver testing

UR - https://www.scopus.com/pages/publications/85116276385

UR - https://www.scopus.com/record/pubmetrics.uri?eid=2-s2.0-85116276385&origin=recordpage

U2 - 10.1145/3468264.3468540

DO - 10.1145/3468264.3468540

M3 - RGC 32 - Refereed conference paper (with host publication)

SN - 978-1-4503-8562-6

SP - 1141

EP - 1153

BT - ESEC/FSE 2021

PB - Association for Computing Machinery

T2 - 29th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2021

Y2 - 23 August 2021 through 28 August 2021

ER -

Skeletal approximation enumeration for SMT solver testing

Abstract

Conference

Funding

Research Keywords

RGC Funding Information

Access Output

Other Access Options

Permanent Link

Other Files and Links

Fingerprint

Cite this