Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution)
Zsófia Ádám, Gyula Sallai, Ákos Hajdu
Abstract
Abstract 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.
Topics & Concepts
Computer sciencePredicate abstractionModel checkingReachabilityProgramming languageToolchainTransformation (genetics)AbstractionSoftwareTheoretical computer sciencePhilosophyChemistryGeneBiochemistryEpistemologyFormal Methods in VerificationSoftware Reliability and Analysis ResearchSoftware Testing and Debugging Techniques