Shallow Finite State Verification:
	     Abstraction Techniques and Complexity Results

			     G. Ramalingam
		    IBM T.J. Watson research Center

The desire for more reliable software has led to increasing interest
in extended static checking: statically verifying whether a program
satisfies certain desirable properties. A technique that has received
particular attention is that of finite state or typestate verification.
In this model, objects of a given type may exist in one of several states;
the operations permitted on an object depend on the state of the object,
and the operations may potentially alter the state of the object. The goal
of typestate verification is to statically determine if the execution of a
given program may cause an operation to be performed on an object
in a state where the operation is not permitted. Typestate verification
can thus be used to check that objects satisfy certain kinds of temporal
properties; for example, that an object is not used before it is 
initialized, or that a file is not used after it is closed.

In this talk, I 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.  I will present 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.