Lics

IEEE Symposium on Logic in Computer Science

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

Third Annual IEEE Symposium on

Logic in Computer Science (LICS 1988)

Paper: On the existence of effective Hoare logics (at LICS 1988)

Authors: Michal Grabowski Hardi Hungar

Abstract

Every proof system for (partial) correctness yields an enumeration procedure for correctness assertions. Other researchers have proved results on the existence of (sound and complete) enumeration procedures for assertions about programs from an acceptable programming language where the assertion language is first-order logic. It is shown that some of the assumptions are stronger than necessary, whereas others must not be weakened. Two novel procedures are given that work for more interpretations with a smaller oracle than those known up to now

BibTeX

  @InProceedings{GrabowskiHungar-Ontheexistenceofeff,
    author = 	 {Michal Grabowski and Hardi Hungar},
    title = 	 {On the existence of effective Hoare logics},
    booktitle =  {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)},
    year =	 {1988},
    month =	 {July}, 
    pages =      {428--435},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski