Program review is an effective technique for detecting faults in software systems by reading and analyzing program code. However, challenges still remain in providing systematic and rigorous review techniques. We have recently developed a rigorous review approach and a software tool that provide reviewers with support in analyzing whether a program accurately implements the functions and properties defined in its specification. In this paper, we describe an empirical study of the application of our review approach and tool to a software system for automated teller machines (ATMs). We also discuss the effectiveness of the review approach, as well as some weaknesses, based on the results of our study, and suggest potential solutions to the problems encountered during the study.