Solving reachability problems on data-aware workflows

Recent advances in the field of Business Process Management (BPM) have brought about several suites able to model data objects along with the traditional control flow perspective. Nonetheless, when it comes to formal verification there is still a lack of effective verification tools on imperative data-aware process models and executions: the data perspective is often abstracted away and verification tools are often missing.