Title:   A Verifier for Interactive, Data-Driven Web Services
Speaker: Alin Deutsch
         (joint work with Monica Marcus, Liying Sui, Victor Vianu and Dayou Zhou)

Abstract:

The talk will present our new model of data-driven Web services
provided by Web sites interacting with users or applications.
The Web site can access an underlying database, as well as state
information updated as the interaction progresses, and receives user input.
The structure and contents of Web pages, as well as the actions to be taken,
are determined dynamically by querying the underlying database as well as the state and inputs.
For this model, we address the problem of verifying
that the web service satisfies desirable properties.
These properties concern the sequences of events
(inputs, states, and actions) resulting from the interaction,
and are expressed in linear temporal logics.

The talk is structured in two parts.

-  First, we establish under what conditions automatic verification
   of such properties is possible and provide the complexity of verification.
   This brings into play a mix of techniques from logic and automatic verification.
-  Next, we present our implementation of a verification tool,
   whose name we hope you will help pick.
   The verifier incorporates several key heuristics, which
   help us bridge the gap from "decidable, but impractical",
   to "feasible within a few hours" and finally
   to "feasible within a few seconds".
   We will report on favorable preliminary experimental results
   (and will keep mum about the unfavorable ones :)

No prior knowledge on automatic verification is assumed.