Paper: Program Correctness on Finite Fields (at LICS 1986)

Authors: László Csirmaz Bradd Hart

Abstract

An asserted program is presented whose correctness is provable by the Floyd-Hoare-Naur method in each finite field separately, which, however, admits no universal derivation, i.e. on which would work on all but finitely many fields of a given characteristic. Also it is proved in general that if 'executing a program twice with the same input, the outputs agree' is a provable property, then the output of the program is first order definable from the input.

BibTeX

  @InProceedings{CsirmazHart-ProgramCorrectnesso,
    author = 	 {László Csirmaz and Bradd Hart},
    title = 	 {Program Correctness on Finite Fields},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {4--10},
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }