Exploratory Analysis of the Performance of a Configurable CEGAR Framework

CímExploratory Analysis of the Performance of a Configurable {CEGAR} Framework
Közlemény típusaConference Paper
Kiadás éve2017
SzerzőkHajdu, Á., and Micskei, Z.
Konferencia neveProceedings of the 24th PhD Mini-Symposium
KiadóBudapest University of Technology and Economics, Department of Measurement and Information Systems

Formal verification techniques can check the correctness of systems in a mathematically precise way. However, their computational complexity often prevents their successful application. The counterexample-guided abstraction refinement (CEGAR) algorithm aims to overcome this problem by automatically building abstractions for the system to reduce its complexity. Previously, we developed a generic CEGAR framework, which incorporates many configurations of the algorithm. In this paper we focus on an exploratory analysis of our framework. We identify parameters of the systems and algorithm configurations, overview some possible analysis methods and present preliminary results. We show that different variants are more efficient for certain tasks and we also describe how the properties of the system and parameters of the algorithm affect the success of verification.