Logic in Computer Science (LICS 1991)

Paper: A compositional proof system for dynamic process creation (at LICS 1991)

Authors: F. de Boer

Abstract

A compositional proof systems for a parallel language, P, with dynamic process creation is presented. It is shown how a dynamic system of processes can be described in terms of specifications of the local processes which involve a characterization of their interface with the environment. The proof system formalizes reasoning about these interfaces on an abstraction level that is at least as high as that of the programming language. The programming language P is described, and two assertion languages, the local one and the global one, are defined. The proof system is described and its soundness and completeness are discussed

BibTeX

  @InProceedings{deBoer-Acompositionalproof,
    author = 	 {F. de Boer},
    title = 	 {A compositional proof system for dynamic process creation},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1991},
    year =	 1991,
    editor =	 {Giles Kahn},
    month =	 {July}, 
    pages =      {399--405},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }