Workflows describe sequences of tasks to achieve goals. These sequences can contain decisions, loops, and parallelisations and are, therefore, similar to computer programs. Experts in the domain of workflow application usually design these workflows. However, these experts are rarely IT experts. For this reason, after automation by a computer, workflows can exhibit undesired behaviors. Such behaviors can be expensive and dangerous and should be avoided. The notion of soundness describes the absence of the undesired behaviors of deadlocks and abundances. The state of the art in workflow verification can detect such behaviors, but gives no indication of causes, does not provide detailed diagnostic information, or is slow. This article introdu...