Abstract: We present recent work at UC San Diego on the verification of compositions of Web Service peers that interact asynchronously by exchanging messages. Each peer can be viewed as a data-aware reactive system. It has access to a local database and reacts to user input and incoming messages by performing various actions and sending messages. The reaction is described by queries over the database, internal state, user input and received messages. We consider the verification of correctness properties expressed in an extension of first-order logic with linear-time temporal operators, and map the boundary of verification decidability, showing that it includes expressive classes of compositions and properties. We also address modular verification, in which the correctness of a composition is predicated on the properties of its environment. The results rely on a novel coupling of model-checking and database techniques. Finally, we present encouraging experimental results on verification of single peers. These suggest that automatic verification may be practically feasible for a large class of data-aware Web services.This is joint work with Alin Deutsch, Liying Sui, and Dayou Zhou.

Short Bio: Victor Vianu received his PhD in Computer Science from the University of Southern California in 1983. Since then, he has been on the faculty at UC San Diego and is now Professor of Computer Science. His interests include database theory, logic and complexity, and Web data. His most recent research focuses on static analysis of XML-based systems, and specification and verification of Web services. Vianu’s publications include over 80 refereed research articles and a graduate textbook on database theory. He has given numerous invited talks, is a member of several editorial boards, and served as General Chair of SIGMOD and Program Chair of the PODS and ICDT conferences. He was elected Fellow of the ACM in 2006.