Compositional execution semantics for business process verification.

•We define a complete execution semantics of BPEL through a new methodology.•We verify important correctness properties using business process models.•We test our BPEL to BIP translation tool in mid-scale programs and their verification.•Translation times grow linearly to the number of states in the generated model.•The translator, the verification utilities and our experimental setting are online.