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