@inproceedings{wensley1978sift,
author = {Wensley, John H. and Lamport, Leslie and Goldberg, Jack and Green, Milton W. and Levitt, Karl N. and Melliar-Smith, P. M. and Shostak, Robert E. and Weinstock, Charles B.},
title = {SIFT: Design and Analysis of a Fault-Tolerant Computer for Aircraft Control},
booktitle = {Proceedings of the IEEE 66},
year = {1978},
month = {October},
abstract = {When it became clear that computers were going to be flying commercial aircraft, NASA began funding research to figure out how to make them reliable enough for the task. Part of that effort was the SIFT project at SRI. This project was perhaps most notable for producing the Byzantine generals problem and its solutions, first reported in [41].

This paper gives an overview of the complete SIFT project, which included designing the hardware and software and formally verifying the system's correctness. It announces the results that appear in [41]. It also is a very early example of the basic specification and verification method I still advocate: writing a specification as a state-transition system and showing that each step of the lower-level specification either implements a step of the higher-level one or is a "stuttering" step that leaves the higher-level state unchanged. The paper doesn't mention the use of an invariant, but that was probably omitted to save space.

This paper was a group effort that I choreographed in a final frenzy of activity to get the paper out in time for the issue's deadline. I don't remember who wrote what, but the section on verification seems to be my writing.},
url = {http://approjects.co.za/?big=en-us/research/publication/sift-design-analysis-fault-tolerant-computer-aircraft-control/},
pages = {1240-1255},
volume = {10},
edition = {Proceedings of the IEEE 66},
}