Artifact-centric systems are a recent paradigm to model and implement
business workflows. They describe data, processes, internal and external agents and include mechanisms for data hiding and access control. GSM is a language for the implementation of artifact-centric systems. Since GSM programs have infinitely many states, their verification is challenging. We here present a predicate abstraction technique that enables us to verify GSM programs against rich
specifications built on an epistemic, first-order variant of the µ-calculus. We give the theoretical underpinnings of the technique and present
GSMC, the first model checker for GSM that implements SMT-based, three-valued abstraction for GSM.