Pointer Structures

In many applications, notably under object oriented proramming, there arise highly complex pointer structures; their careless use is a frequent cause of severe system errors. Hence a formal way of establishing safety is of particular interest for this area. It turns out that a special variant of Kleene algebra provides a solid and concise algebraic basis for this.
It allows also the description of shared mutable data structures as they are used in separation logic.