Formal verification is becoming more prevalent, especially in the development of safety-critical systems, where mathematically precise proofs are required to ensure suitability and faultlessness. However, a major drawback of formal methods is their high computational complexity. This also holds for model checking, one of the most prevalent formal verification techniques. Model checking aims to automatically verify a system by exhaustively (explicitly or symbolically) analyzing its possible behaviors. However, relatively small systems can have an unmanageably large or even infinite number of behaviors. There are several existing approaches to handle this problem, but as the complexity of the models increases, new and more efficient algorithms are required.
A widely used technique to overcome the former problem is Counterexample-Guided Abstraction Refinement (CEGAR). CEGAR-based approaches work on an abstraction of the model, which is computationally easier to handle. A common abstraction scheme is to over-approximate the set of behaviors by systematically relaxing constraints in the model. However, the result of the algorithm may be imprecise due to the coarseness of the abstraction. In such cases, the abstraction has to be refined. CEGAR-based approaches usually start with a coarse abstraction to minimize computational cost and apply refinement until a precise result is obtained.
In my work I examine the literature and the theoretical background of model checking of transition systems using CEGAR-based approaches. I present first order and temporal logic for formalizing systems and requirements, and I analyze two CEGAR algorithms based on different subtypes of over-approximation. I also examine a handful of related techniques that can make CEGAR more efficient, including SAT/SMT solving, interpolation and lazy abstraction. I also propose a new algorithm that combines the advantages of these approaches and techniques. I have implemented these algorithms in order to evaluate and compare their performance. Analysis of the measurement results highlights the advantages and shortcomings of the algorithms for several types of models.