Introduction to CEGAR —Counter-Example Guided Abstraction Refinement

• Main Authors: M. U. Mandrykin, V. S. Mutilin, A. V. Khoroshilov
• Format: Article
• Language: English
• Published: Ivannikov Institute for System Programming of the Russian Academy of Sciences 2018-10-01
• Series: Труды Института системного программирования РАН
• Subjects: статическая верификация; предикатная абстракция; проверка моделей; уточнение абстракции по контрпримерам; интерполяция крейга; крупноблочное кодирование
• Online Access: https://ispranproceedings.elpub.ru/jour/article/view/959
• ISSN: 2079-8156; 2220-6426

Precision, completeness and scalability of static verification tools have dramatically improved over the last decade. In particular, automatic checking of moderate-sized software systems has been made possible due to development of CEGAR — Counter-Example Guided Abstraction Refinement. This approach is used in such tools as SLAM, BLAST, SATABS, and CPAchecker. The paper presents an extended review of predicate abstraction-based CEGAR. It provides an introduction to the general principles of CEGAR and describes some implementation details of CEGAR in BLAST and CPAchecker. In particular, the paper concerns deciding the reachability problem for C programs by means of symbolic predicate abstraction. The set of predicates for the abstraction is obtained by Craig interpolation of the logical formulas representing the counterexample traces being discovered during the analysis. This technique is explained by two examples analyzed step-by-step both in intuitive and in formal manner. The explanation proceeds from a number of greatly simplified programs employing a very restricted subset of C language features (e.g. using only a finite set of integer variables) to more complicated programs of arbitrary size with pointers, heap allocations and bit operations. In terms of considered abstract domains the paper describes the simplest fine-grained Cartesian abstraction and a coarse-grained Boolean abstraction with adjustable block encoding. The paper also includes small discussions on common issues arising from verification of real industrial C codebase and current capabilities of existing decision procedure implementations.