Verifying data refinements using a model checker
scientific article; zbMATH DE number 5073784