Proving the correctness of a flight-director program for an airborne minicomputer
Ward Douglas Maurer · ACM SIGMINI Newsletter · 1976
Over the past five years, our research efforts have been devoted in large part to developing techniques for proving the correctness of assembly-language and machine-language programs running on actual computers. In this paper, we report upon an effort to put this work into practice by proving the correctness of a program written for the Litton C4000 airborne computer. This includes overflow analysis, non-self-modification analysis, round-off and truncation analysis, fixed-point scaling considerations, and analysis of the subroutine parameter and return-address conventions used in the given program. The basic method we use is the inductive assertion method of (Floyd, 1967), suitably modified and extended for application to a machine-language situation.