How can a computer program developer ensure that a program actually implements its intended purpose? This article describes a method for checking the correctness of certain types of computer programs. The method is used commercially in the development of programs implemented as integrated circuits, and is applicable to the development of “control-intensive” software programs as well. “Divide-and-conquer” techniques central to this method apply to a broad range of program verification methodologies.