General Terms Verification

For a single object, many programming errors can be de-tected by specifying the undesirable sequence of events us-ing typestate. However, since objects interact with one an-other, defining temporal specifications only for a single ob-ject is too restrictive. In our research, we are interested in ex-tending techniques from static typestate verification to static verification of multi-object temporal specifications