On logics of aliasing

Abstract

In this paper we investigate the existence of a deductive verification method based on a logic that describes pointer aliasing. The main idea of such a method is that the user has to annotate the program with loop invariants, pre- and post-conditions. The annotations are then automatically checked for validity by propagating weakest preconditions and verifying a number of induced implications. Such a method requires an underlying logic which is decidable and has a sound and complete weakest precondition calculus. We start by presenting a powerful logic (wAL) which can describe the shapes of most recursively defined data structures (lists, trees, etc.) has a complete weakest precondition calculus but is undecidable. Next, we identify a decidable subset (pAL) for which we show closure under the weakest precondition operators. In the latter logic one loses the ability of describing unbounded heap structures, yet bounded structures can be characterized up to isomorphism. For this logic two sound and complete proof systems are given, one based on natural deduction, and another based on the effective method of analytic tableaux. The two logics presented in this paper can be seen as extreme values in a framework which attempts to reconcile the naturally oposite goals of expressiveness and decidability. © Springer-Verlag 2004.