@inbook {tacas2021,
	title = {Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution)},
	booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
	series = {Lecture Notes in Computer Science},
	volume = {12652},
	year = {2021},
	note = {(Accepted)},
	publisher = {Springer},
	organization = {Springer},
	abstract = {<p>
	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.</p>
},
	author = {Zs{\'o}fia {\'A}d{\'a}m and Gyula Sallai and {\'A}kos Hajdu},
	editor = {Jan Friso Groote and Kim G. Larsen}
}
