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

We are currently interested in the verification of concurrent programs that manipulate dynamic memory. Our approach is based on two fundamental blocks:

• we use explicit regions (instead of Separation Logic) to reason about data structures allocated on the heap. This provide us a more flexible manner of describing heap structure, at the price of some program annotations.

• we use general verification diagrams. A verification diagram is a sound and complete method to represent proofs of temporal property over reactive system. The verification process using verification diagrams is reduced to a collection of first-order verification conditions, together with a few (decidable) tests over finite graphs.

Our current goal is to be able to automatically check the validity of the verification conditions discharged from a verification diagram. As concurrents datatype keep in memory a set of nodes and pointers with some specific layout, the generated verification conditions can be expressed as predicates to specific theories. In the case of concurrent lists a decision procedure capable of reasoning about memory cells, regions and ideal lists is needed.

This Tuesday I will (try to) give a brief description of the most recent results in decision procedures of singly linked lists and some extensions.