On Logics of Aliasing

Abstract. In this paper we investigate the existence of a deductive veri cation 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 de ned 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 l...

• Type: Conference
• Year: 2004
• Where: SAS
• Authors: Marius Bozga, Radu Iosif, Yassine Lakhnech
• Keywords: Complete Weakest Precondition, Formal Methods, SAS 2004, Weakest Precondition, Weakest Precondition Calculus