SYMBIOTIC-WITCH 2: More Efficient Algorithm and Witness Refutation? (Competition Contribution)

被引：4

作者：

Ayaziova, Paulina ^{[1
]}

Strejcek, Jan ^{[1
]}

机构：

[1] Masaryk Univ, Brno, Czech Republic

来源：

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2023 | 2023年 / 13994卷

关键词：

D O I：

10.1007/978-3-031-30820-8_30

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

The new version of the witness validator Symbiotic-Witch follows more precisely the (fixed version of the) semantics of verification witnesses. This makes the tool more efficient as it can benefit from sink nodes. Further, the tool can now refute a witness. To sum up, Symbiotic-Witch 2 can confirm or refute violation witnesses of reachability safety, memory safety, memory cleanup, and overflow properties of sequential C programs.

引用

页码：523 / 528

页数：6

共 10 条

[1] [Anonymous], 2008, P 8 USENIX C OPERATI
[2] Ayaziova P., 2022, TOOLS ALGORITHMS CON
[3] Ayaziova Paulina, 2022, Zenodo, DOI 10.5281/ZENODO.7630406
[4] Beyer D., 2023, LNCS
[5] Beyer Dirk, 2023, Zenodo, DOI 10.5281/ZENODO.7627829
[6] Verification Witnesses
Beyer, Dirk
Dangl, Matthias
Dietsch, Daniel
Heizmann, Matthias
Lemberger, Thomas
Tautschnig, Michael
[J]. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2022, 31 (04)
[7] Chalupa M., TOOLS ALGORITHMS CON
[8] Z3: An efficient SMT solver
de Moura, Leonardo
Bjorner, Nikolaj
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 337 - 340
[9] Heizmann M., TOOLS ALGORITHMS CON
[10] SYMBOLIC EXECUTION AND PROGRAM TESTING
KING, JC
[J]. COMMUNICATIONS OF THE ACM, 1976, 19 (07) : 385 - 394

← 1 →