Modeling and verifying business processes and choreographies through the abductive proof procedure SCIFF and its extensions

In this article we survey our recent research activity concerning the use of logic programming, and in particular of abduction, for interaction specification and verification in several domains. We outline relevant results in the areas of multi-agent systems, argumentation, web services choreographies and business processes.