Proving the correctness of a flight-director program for an airborne minicomputer
- 4 March 1976
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 11 (4) , 103-108
- https://doi.org/10.1145/872740.807101
Abstract
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 sub-routine 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.This publication has 3 references indexed in Scilit:
- Some correctness principles for machine language programs and microprogramsPublished by Association for Computing Machinery (ACM) ,1974
- An axiomatic basis for computer programmingCommunications of the ACM, 1969
- Assigning meanings to programsPublished by American Mathematical Society (AMS) ,1967