Abstract

Recently, an extension to separation logic has been proposed to make it simpler to verify the correct functioning of concurrent programs. Until now, one usually checks whether data races are absent using for example the de facto standard Owicki-Gries. However, verifying absence of data races does not scale, moreover functional properties cannot be verified. Therefore, histories are added to a program to take its state into account. Histories are updated if values are modified. Using this information, it can be verified that a method behaves as specified. In this paper, this proposed method is used to verify with VerCors some larger concurrent examples to find out if it is as simple as typically used techniques for data race checking are, while being able to verify even functional requirements of a method. It turns out that verifying those examples is doable, but at this moment not trivial. In the future this will be improved.

Additional Resources

1. The paper