Formal verification of imperative programs provides a high guarantee of software quality, but it is usually a human intensive technique. Hence, it is only used in practice for the most critical parts.

Concurrent algorithms are difficult to reason about since their execution consists of different interleavings that may lead to unpredictable and erroneous behaviors. The verification problem becomes particularly challenging when the data structures are dynamic and stored in the heap. Our work focuses on the verification of concurrent data-structures, and the multi-threaded programs that use them. In particular we are interested in verifying general temporal properties. This includes not only safety properties (like invariants) but also liveness properties (like program termination). Our approach differs from most of the currently used techniques in three main aspects:

• First, to reason about data structures allocated on the heap, we employ Regional Logic instead of Separation Logic. This provide us a more expressive and detailed way of describing heap structure thanks to the explicit manipulation of regions of memory.

• Second, our work is based on rely-guarantee reasoning, letting us avoid direct reasoning over all possible thread interleavings. This allows us to describe the visible behavior of all parallel executing threads as a more general rely property, thus simplifying the reasoning problem. Since Regional Logic is a classical (first-order) logic, classical rely-guarantee reasoning can be immediately employed. Moreover, we consider dynamic thread creation.

• Third, instead of reducing the proof of a temporal property to a termination problem and discharging this problem into a termination checker, we make use of general verification diagrams. A verification diagram is a sound and complete method to represent a proof of a general temporal property over a reactive system. The validity check of a verification diagram is reduced to a collection of first-order verification conditions together with a few (decidable) tests over finite graphs. This Tuesday I will give a brief introduction to the work we have been carrying out along the last months as well as a short explanation of some small working(?) examples on singly-linked concurrent lists that reveals some benefits of the chosen methodologies.

This is joint work with Cesar Sanchez, Anindya Banerjee and Gilles Barthe.