Verifying pointer programs using separation logic and invariant based programming in Isabelle

In this paper we present a technique based on invariant based programming and separation logic for verifying pointer programs. Invariant based programs are directed graphs where the nodes are called situations and are labeled by predicates (invariants). The edges are called transitions, and are labeled by guarded assignment statements. We represent the situations using Isabelle’s locales. A locale is a theory parameterized by constants and types. The constant parameters are used for modeling the state of the program, and the type parameters are used for obtaining generic programs. The invariants are modeled as locale assumptions (axioms), and the transitions are modeled as locale interpretations. For modeling pointer programs we use separation logic. The final result of this construction is a collection of mutually recursive Isabelle functions that implements the program. We apply this technique to Lindstrom’s algorithm for traversing a binary tree without additional memory.