We consider the problem of typestate verification for
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 verification
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.
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.