|
Published Articles >> Table of Contents >> Abstract
31st IEEE Software Engineering Workshop (SEW 2007)
pp. 204-213
Abstracting Pointers for a Verifying Compiler
Gregory Kulczycki
Heather Keown
Murali Sitaraman
Bruce W. Weide
Full Article Text:
 
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEW.2007.89
Send link to a friend
| Abstract |
|
Gregory Kulczycki Virginia Tech Falls Church, VA, USA gregwk@vt.edu Heather Keown, Murali Sitaraman Clemson University Clemson, SC, USA {hkeown, murali}@cs.clemson.edu Bruce W. Weide The Ohio State University Columbus, OH, USA weide.1@osu.edu Abstract 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 refer- ences and linked data structures. In some situations, pointers are unavoidable; in some others, verification can be simplified through suitable abstractions. Re- gardless, 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 ap- proaches to full verification. One replaces language- supplied indirection with software components whose specifications abstract pointers and pointer- manipulation operations. Another approach uses ab- stract specifications to encapsulate data structures that pointers and references are often used to implement, limiting verification complications to inside the imple- mentations of these components. Using a modular, specification-based tool we have developed for verifi- cation condition generation, we show that full verifica- tion of programs with and without the direct use of pointers can be handled similarly. There is neither a need to focus on selected pointer properties, such as the absence of null references or cycles, nor a need for special rules to handle pointers.
|
 Additional Information
|
Citation:
Gregory Kulczycki, Heather Keown, Murali Sitaraman, Bruce W. Weide,
"Abstracting Pointers for a Verifying Compiler,"
sew,
pp. 204-213,
31st IEEE Software Engineering Workshop (SEW 2007),
2007
|
|
