Verification of Pointers

Abstract

Our recent work links type checking in programming languages to verification based on automata. In this survey, we give an overview of our methods and suggest directions for future research.

In our approach, we view data types as invariants and devise a logical and decidable framework for expressing global properties of a store consisting of records and pointers.

We can express common properties, for example about doubly-linked lists and their algorithms. Such properties seemed to have called for a full Hoare logic beyond the reach of type checking and decidability.

Our work is based on monadic second-order logic. Thus verification boils down to calculations on finite-state automata. This raises specific questions about combinatorial techniques for representing state spaces if these calculations are ever to be carried out on more than simple examples.