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
  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,}


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 ... BibTeX

Printed Edition

Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, January 1979. ACM 1979 BibTeX

Online Edition: ACM Digital Library


Copyright © Sat May 16 23:34:35 2009 by Michael Ley (