Federico Chesani bib references

@INPROCEEDINGS{PPDP06,
  AUTHOR = {Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Marco Montali},
  TITLE   = {An Abductive Framework for A-Priori Verification of Web Services},
  BOOKTITLE = {Proceedings of the Eighth Symposium on Principles and Practice of Declarative Programming, July 10-12, 2006, Venice, Italy},
  YEAR = {2006},
  editor = {Michael Maher},
  publisher = {ACM Press},
  month = jul,
  url = "http://www.dsi.unive.it/ppdp2006/",
  pages = {39--50},
  isbn = {1-59593-388-3},
  address = {New York, USA},
  organization = {Association for Computing Machinery (ACM), Special Interest Group on Programming Languages (SIGPLAN)},
  abstract = "
Although stemming from very different research areas, Multi-Agent Systems (MAS) and Service Oriented Computing (SOC) share common topics, problems and settings.
One of the common problems is the need to formally verify the conformance of individuals (Agents or Web Services) to common rules and specifications (resp. Protocols/Choreographies), in order to provide a coherent behaviour and to reach the goals of the user.

In previous publications, we developed a framework, SCIFF, for the automatic verification of compliance of agents to protocols. The framework includes a language based on abductive logic programming and on constraint logic programming for formally defining the social rules;  suitable proof-procedures to check on-the-fly and a-priori the compliance of agents to protocols have been defined.

Building on our experience in the MAS area, in this paper we make a first step towards
the formal verification of web services conformance to choreographies. We adapt the SCIFF framework for the new settings, and propose a heir of SCIFF, the framework AL$^l$LoWS (Abductive Logic Web-service Specification).
AL$^l$LoWS comes with a language for defining formally a choreography and a web service specification. As its ancestor, AL$^l$LoWS has a declarative and an operational semantics. We show examples of how AL$^l$LoWS deals correctly with  interaction patterns previously identified. Moreover, thanks to its constraint-based semantics, AL$^l$LoWS deals seamlessly with other cases involving constraints and deadlines.",
}