Title: Specification and Automatic Verification of Frame Properties for Java-like Programs (Specificatie en automatische verificatie van frame eigenschappen voor Java-achtige programma's)
Other Titles: Specification and Automatic Verification of Frame Properties for Java-like Programs
Authors: Smans, Jan; M0116852
Issue Date: 26-May-2009
Abstract: Program verification is a technique for proving that a program satisfies its specification. An important problem in the verification of imperative programs with shared mutable state is the frame problem in the presence of data abstraction. That is, one must be able to specify and verifyupper bounds on the set of memory locations a method can read and writewithout revealing the method's implementation.This thesis makes two contributions that both address this problem in the context of Java. Firstly, we demonstrate that the dynamic frames approach, an existing solution to the frame problem, can be applied to Java and is amenable to automatic, static verification. Secondly, we propose a variant of the dynamic frames approach, called implicit dynamic frames, where frame information is inferred from method preconditions. The latter approach improves upon the original dynamic frames approach by making contracts more concise and by ensuring that less proof obligations must be discharged by the verifier. Both techniques have been proven sound and are implemented in verifier prototypes. Those prototypes have been used to automatically verify several challenging programs used in relatedwork.
Table of Contents: 1. Introduction
2. Dynamic Frames
3. Implicit Dynamic Frames
4. Conclusion
Publication status: published
KU Leuven publication type: TH
Appears in Collections:Informatics Section

Files in This Item:
File Status SizeFormat
thesis-jansmans.pdf Published 651KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.