27-Apr-2017: CPAchecker-BAM-BnB and BLAST 2.7.3 at SV-COMP'2017

CPAchecker-BAM-BnB and BLAST 2.7.3 were presented at the 6th International Competition on Software Verification (SV-COMP) held at TACAS 2017 in Uppsala, Sweden.

CPAchecker-BAM-BnB tool is an improvement of CPAchecker in the block abstraction memorization and memory model. The tool has got fifth place in Software Systems category.

The new BnB memory model was presented in the talk. The memory model used by default divides memory into regions by types of variables. So the the pointer variables of different types were considered as not to point to the same memory. For the others a formula is constructed which tells whether they point to the same memory or not. Then the formula is solved by a special component called solver. The plenty of pointers used in the programs require large amount of resources.

The new model divides memory into more non-intersecting regions, that decreases resources demands to the solver. For the pointers which are structure fields: if there is no address taken in the program then they are not aliases and can be placed into disjoint regions. Thus the formulas in the analysis become easier and the solver load decreases.

The results are two-fold. On the one hand, the simplification of formulas leads to faster solving of verification tasks. On the other hand, for some verification tasks the time increased, because the analysis became more conservative: some aliases are disappeared.

In the second talk we presented recommendations for using static verification tools in the area of Linux driver verification. At first, for visualization purposes we suggested to include important details into correctness and violation witnesses, produced by the tools. So the tools providing such information can use unified visualization mechanism.

Second suggestion concerns preparation of verification benchmarks for the competition. Currently in many tasks, especially in Linux drivers, external undefined functions are used that causes undefined behavior. To specify the behaviour of such functions we propose to have a notion of on-demand memory, having memory values defined by memory access expressions. Such memory can be safely dereferenced, at the same time we do not assume a particular shape of that memory, so we do not loose reachable paths.