Paper: Complexity bounds of Hoare-style proof systems (at LICS 1991)

Authors: Hardi Hungar

Abstract

A refinement of the result that there is no sound and relatively complete proof system for a programming language if its partial correctness theory is undecidable even in finite interpretations is presented. By taking into account the computational complexity of this problem, information about structural properties of proof systems for a given programming language is obtained. The key in the proofs is the notion of an interpretation independent proof system. It is shown that ordinary systems are interpretation independent, but that such systems are limited in their power. It is proven that they can deal successfully only with assertions whose sets of finite models are in NPTIME. Some assertions about programs from E.M. Clarke's (1979) language L4 have a more complex (but still decidable) set of finite models. This substantiates why it was difficult to give a satisfactory proof system for this language. The author explains which features of Clarke's proof system allow problems of such complexity to be treated

BibTeX

  @InProceedings{Hungar-ComplexityboundsofH,
    author = 	 {Hardi Hungar},
    title = 	 {Complexity bounds of Hoare-style proof systems},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)},
    year =	 {1991},
    month =	 {July}, 
    pages =      {120--126},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }