PDF:
Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution)
| Cím | Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution) |
| Közlemény típusa | Book Chapter |
| Kiadás éve | 2021 |
| Szerzők | Ádám, Z., Sallai, G., and Hajdu, Á. |
| Szerkesztő | Groote, J F., and Larsen, K. G. |
| Könyvcím | Tools and Algorithms for the Construction and Analysis of Systems |
| Sorozatcím | Lecture Notes in Computer Science |
| Kötet | 12652 |
| Kiadó | Springer |
| Összefoglalás | 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 SV-COMP 2021, a portfolio of BMC, explicit-value analysis, and predicate abstraction is applied sequentially in this order. |
| Jegyzetek | (Accepted) |
