Proving Program Termination.

Saved in:

Bibliographic Details
Title:	Proving Program Termination.
Authors:	COOK, BYRON^1,2, PODELSKI, ANDREAS³, RYBALCHENKO, ANDREY⁴
Source:	Communications of the ACM. May2011, Vol. 54 Issue 5, p88-98. 11p. 1 Illustration, 11 Diagrams.
Subjects:	Computer software termination, Decidability (Mathematical logic), Ramsey theory, Computable functions, Computer logic, Mathematical logic
Abstract:	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.
Database:	Engineering Source

Description
Abstract:	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.
ISSN:	00010782
DOI:	10.1145/1941487.1941509