Specification and verification of a network mail system

  • Susan S. Owicki
II. Program Verification
Part of the Lecture Notes in Computer Science book series (LNCS, volume 69)


Techniques for describing and verifying modular systems are illustrated using a simple network mail problem. The design is presented in a top-down style. At each level of refinement, the specifications of the higher level are verified from the specifications of lower level components.


Local User Error Message Message Delivery Exit Condition Proof Outline 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Owicki, S., Specifications and Proofs for Abstract Data Types in Concurrent Programs, in this volume.Google Scholar
  2. [2]
    Brinch Hansen, P., Network, a Multiprocessor Program. IEEE Trans on Software Engineering, v. 4, no. 3 (May, 1978) 194–199.Google Scholar
  3. [3]
    Ambler, A., et al., A Language for Specification and Implementation of Verifiable Programs. Proc. of an ACM Conference on Language Design for Reliable Software, SIGPLAN Notices v. 12, n.3 (also Operating Systems Review v. 11, n.2, and Software Engineering Notes, v.2, n.2) (1977) 1–10.Google Scholar
  4. [4]
    Andrews, G., Modula and the Design of a Message Switching Communications System. TR78-329, Cornell University, Computer Science Dept. (1978)Google Scholar
  5. [5]
    Owicki, S., Verifying Parallel Programs with Resource Allocation. Proc. International Conference on Math. Studies of Information Processing, Kyoto, Japan (1978).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1979

Authors and Affiliations

  • Susan S. Owicki
    • 1
  1. 1.Digital Systems LaboratoryStanford UniversityStanford

Personalised recommendations