M. Clavel, M. Egea, and M. A. García de Dios, “Checking Unsatisfiability for OCL Constraints”, ECEASST, vol. 24, Jan. 2010.