Author:

Keywords:

verification, frame problem, Java, dynamic frames

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.