Lics

ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

First Annual IEEE Symposium on

Logic in Computer Science (LICS 1986)

Paper: A Semantically Based Proof System for Partial Correctness and Deadlock in CSP (at LICS 1986)

Authors: Stephen D. Brookes

Abstract

We build a semantically based assertion language and proof system for partial correctness and deadlock of CSP programs. The assertions are tree-structured and have two types of leaf nodes so that we can distinguish between termination and deadlock. We define syntactic sequential and parallel composition of assertions. The proof system is syntax-directed, and does not require the use of auxiliary variables. The proof rule for parallel composition does not require constraints such as interference-freedom or a cooperation test. It is possible to reason about correctness and deadlock-freedom together, so that we do not require separate proofs of freedom from deadlock and partial correctness.

BibTeX

  @InProceedings{Brookes-ASemanticallyBasedP,
    author = 	 {Stephen D. Brookes},
    title = 	 {A Semantically Based Proof System for Partial Correctness and Deadlock in CSP},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {58--65},
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2022-10-3113:49
Sam Staton