Proving Program Termination.

The article discusses methods for testing whether a computer program will terminate or not. This involves methods of coping with a mathematical problem that was proved to be formally undecidable by the pioneering computer scientist Alan Turing. It is known as the halting problem, or program terminat...

Descripción completa

Detalles Bibliográficos
Publicado en:Communications of the ACM Vol. 54; no. 5; pp. 88 - 99
Autores principales: COOK, BYRON, PODELSKI, ANDREAS, RYBALCHENKO, ANDREY
Formato: Artículo
Publicado: Association for Computing Machinery May2011
Materias:
Acceso en línea:Ver este registro en EBSCOhost
fields @attributes:
  recordID: 1
pdfLink:
plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=60863980&site=ehost-live
header:
  @attributes:
    shortDbName: hlh
    uiTerm: 60863980
    longDbName: Humanities International Complete
    uiTag: AN
  controlInfo:
    bkinfo:
    jinfo:
      jid:
        00010782
        ACM
      jtl: Communications of the ACM
      issn: 00010782
      maglogo: N
    pubinfo:
      dt: May2011
      vid: 54
      iid: 5
      pid: 68
      pub: Association for Computing Machinery
    artinfo:
      ui:
        60863980
        10.1145/1941487.1941509
      ppf: 88
      ppct: 11
      formats:
      tig:
        atl: Proving Program Termination.
      aug:
        au:
          COOK, BYRON
          PODELSKI, ANDREAS
          RYBALCHENKO, ANDREY
        affil:
          Principal Researcher at Microsoft's research laboratory at Cambridge University.
          Professor of computer science at Queen Mary, University of London, England.
          Andreas Podelski is a professor of computer science, University of Freiburg, Germany.
          Andrey Rybalchenko is a professor of computer science, Technische Universität München, Germany.
      su:
        Computer software termination
        Decidability (Mathematical logic)
        Ramsey theory
        Computable functions
        Computer logic
        Mathematical logic
      sug:
        subj:
          Computer software termination
          Decidability (Mathematical logic)
          Ramsey theory
          Computable functions
          Computer logic
          Mathematical logic
      ab: The article discusses methods for testing whether a computer program will terminate or not. This involves methods of coping with a mathematical problem that was proved to be formally undecidable by the pioneering computer scientist Alan Turing. It is known as the halting problem, or program termination problem. Although a yes or no answer cannot always be supplied, the article presents a method, based on Ramsey theory, which provides yes or no answers often enough to be useful. The method can be scaled up to large programs by constructing modular termination arguments.
      pubtype: Periodical
      doctype: Article
      src: R
    language: English
    refInfo:
    copyright:
      @attributes:
        flag: Y
      dt:
        @attributes:
          year: 2011
    holdings:
      @attributes:
        islocal: N