Concurrent and distributed systems based on message passing have become important drivers of our technological advancement. Their programming requires the integration of communicating processes, at the heart of which we find the notion of choreography: a document that prescribes the communications that processes should perform in order to reach a common goal. We say that a system has the property of choreography compliance if the interactions that take place among processes follow the agreed-upon choreography.