Validating temporal properties of interacting objects.

For a single object, many programming errors can be detected by specifying the undesirable sequence of events using typestate. However, since objects interact with one another, defining temporal specifications only for a single object is too restrictive. In our research, we are interested in extending techniques from static typestate verification to static verification of multi-object temporal specifications.