Modeling memory with uninterpreted functions for predicate abstractions

One of the key problems in modern static verification methods is a precise model for semantics of expressions containing pointers. The trustworthiness of the verification verdict highly depends on the analysis of these expressions. In the paper, we describe the verification methods with memory models based on uninterpreted functions, allowing to analyze programs containing expressions with pointers, including pointers to structures, arrays and pointer arithmetic. The approach is limited finite array size and finite recursion depth for dynamic data structures. The method was implemented in CPAchecker tool, based on CEGAR with boolean predicate abstractions and Craig interpolation for inferring new predicates used in abstraction refinement. For solving safisfability of path formulas and Craig interpolation CPAchecker uses interpolation solvers supporting theories of linear integer and real inequalities and equalities with uninterpreted functions. In the method, the memory state is represented as uninterpreted function mapping some variable addresses in memory to its values. After each write to memory for a pointer the version of uninterpreted function is changed. The experiments were performed on the benchmarks of International Competition on Software Verification (SV-COMP'2016) containing industrial size benchmarks of device drivers of Linux operating system. On these benchmarks, the method demonstrates reasonable verification times, reducing the number of missed defects and false alarms. Among the future work directions we consider deviding memory into region thus having a separate uninterpreted for each region.