Typestate Verification: Abstraction Techniques and Complexity Results (report title was: Shallow Finite State Verification)

We consider the problem of verifying finite state properties of shallow programs; i.e., programs where pointers from program variables to heap-allocated objects are allowed, but where heap-allocated objects may not themselves contain pointers. We prove a number of results relating the complexity of such verification problems to the nature of the finite state machine used to specify the property. Some properties are shown to be intractable, but others which appear to be quite similar admit polynomial-time verification algorithms. While there has been much progress on many aspects of automated program verification, we are not aware of any previous work relating the difficulty of finite state verification to properties of the finite state automaton. Our results serve to provide insight into the inherent complexity of important classes of verification problems. In addition, the program abstractions used for the polynomial-time verification algorithms may be of independent interest.