@inproceedings {minisy2019,
	title = {Software Model Checking with a Combination of Explicit Values and Predicates},
	booktitle = {Proceedings of the 26th PhD Mini-Symposium},
	year = {2019},
	month = {01/2019},
	pages = {4{\textendash}7},
	publisher = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},
	organization = {Budapest University of Technology and Economics, Department of Measurement and Information Systems},
	address = {Budapest, Hungary},
	abstract = {<p>
	Formal verification techniques can both reveal bugs or prove their absence in programs with a sound mathematical basis. However, their high computational complexity often prevents their application on real-world software. Counterexample-guided abstraction refinement (CEGAR) aims to improve efficiency by automatically constructing and refining abstractions for the program. There are several existing abstract domains, such as explicit-values and predicates, but different abstract domains are suitable for different kinds of software. Therefore, product domains have also emerged, which combine different kinds of abstractions in a single algorithm. In this paper, we present a new variant of the CEGAR algorithm, which is a combination of explicit-value analysis and predicate abstraction. We perform an experiment with a wide range of software systems and we compare the results to the existing methods. Measurements show that our new algorithm can efficiently combine the advantages of the different domains.</p>
},
	isbn = {978-963-313-314-9},
	doi = {10.5281/zenodo.2597969},
	author = {Bajkai, Dorina Vikt{\'o}ria and {\'A}kos Hajdu},
	editor = {Pataki, B{\'e}la}
}
