Program Verification
01 January 2000
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.