Abstracting Pointers for a Verifying Compiler
Gregory W. Kulczycki, Heather Harton Keown, Murali Sitaraman, Bruce W. Weide · 2007
The ultimate objective of a verifying compiler is to prove that proposed code implements a full behavioral specification. Experience reveals this to be especially difficult for programs that involve pointers or references and linked data structures. In some situations, pointers are unavoidable; in some others, verification can be simplified through suitable abstractions. Regardless, a verifying compiler should be able to handle both cases, preferably using the same set of rules. To illustrate how this can be done, we examine two approaches to full verification. One replaces language-supplied indirection with software components whose specifications abstract pointers and pointermanipulation operations. Another approach uses abstract specifications to encapsulate linked data structures that pointers and references are often used to implement, thereby limiting verification complications to inside the implementations of these components. Both approaches are applied to a sample program previously attacked using lightweight formal methods, focusing on problem-independent pointer properties, such as the absence of null references or cycles. The result is a basis for a compiler capable of full verification.