Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution)

被引：10

作者：

Adam, Zsofia ^{[1
]}

Sallai, Gyula ^{[2
]}

Hajdu, Akos ^{[1
]}

机构：

[1] Budapest Univ Technol & Econ, Budapest, Hungary

[2] SonarSource SA, Geneva, Switzerland

来源：

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

基金：

欧盟地平线“2020”;

关键词：

D O I：

10.1007/978-3-030-72013-1_27

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Gazer-Theta is a software model checking toolchain including various analyses for state reachability. The frontend, namely Gazer, supports C programs through an LLVM-based transformation and optimization pipeline. Gazer includes an integrated bounded model checker (BMC) and can also employ the Theta backend, a generic verification framework based on abstraction-refinement (CEGAR). On SVCOMP 2021, a portfolio of BMC, explicit-value analysis, and predicate abstraction is applied sequentially in this order.

引用

页码：433 / 437

页数：5

共 8 条

[1] Beyer D, 2013, LECT NOTES COMPUT SC, V7793, P146, DOI 10.1007/978-3-642-37057-1_11
[2] Biere A, 1999, LECT NOTES COMPUT SC, V1579, P193
[3] 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
[4] Graf S, 1997, LECT NOTES COMPUT SC, V1254, P72
[5] Efficient Strategies for CEGAR-Based Model Checking
Hajdu, Akos
Micskei, Zoltan
[J]. JOURNAL OF AUTOMATED REASONING, 2020, 64 (06) : 1051 - 1091
[6] Lal Akash, 2012, Computer Aided Verification. Proceedings 24th International Conference, CAV 2012, P427, DOI 10.1007/978-3-642-31424-7_32
[7] Sallai Gy., 2019, LLVM IR-based Transformations for Software Model Checking
[8] Tóth T, 2017, PROCEEDINGS OF THE 17TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD 2017), P176, DOI 10.23919/FMCAD.2017.8102257

← 1 →