Principles of Proving Programs Correct in Gypsy.

Donald I. Good, Richard M. Cohen, James Keeton-Williams: Principles of Proving Programs Correct in Gypsy. POPL 1979: 42-52

@inproceedings{DBLP:conf/popl/GoodC79,
  author    = {Donald I. Good and
               Richard M. Cohen and
               James Keeton-Williams},
  title     = {Principles of Proving Programs Correct in Gypsy},
  booktitle = {POPL},
  year      = {1979},
  pages     = {42-52},
  ee        = {db/conf/popl/GoodC79.html},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Abstract

Concurrency in Gypsy is based on a unique, formal approach to specifying and proving systems of concurrent processes. The specification and proof methods are designed so that proofs of individual processes are totally independent, even when operating concurrently. These methods can be applied both to terminating and non-terminating processes, and the proof methods are well suited to automated verification aids. The basic principles of these methods and their interaction with the design of Gypsy are described.

Copyright © 1979 by the ACM, Inc., used by permission. Permission to make digital or hard copies is granted provided that copies are not made or distributed for profit or direct commercial advantage, and that copies show this notice on the first page or initial screen of a display along with the full citation.

POPL Proceedings Compendium

CDROM Version: Load the CDROM "POPL, The First Ten Years" and ...

Windows: Click the letter of your CD drive
A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
Mac: Click here
UNIX/LINUX: mount the CD and click on the path of your mount point:
/Anthology/Popl or /cdrom