Proving programs terminate using well orderings, Ramsey Theory, and Matrices

William Gasarch

Published: 2011-08-16 | Updated: 2014-11-03

Comments: While this is classified under Combinatorics (to tell combinatorists that someone is using their stuff) it should also be of interest to Logicians and Computer Scientists

Note:

DOI: 10.1016/bs.adcom.2014.12.002

ramsey theory

# BIB PDF ARXIV

Abstract

Many programs allow the user to input data several times during its execution. If the program runs forever the user may input data infinitely often. A program terminates if it terminates no matter what the user does. We discuss various ways to prove that program terminates. The proofs use well orderings, Ramsey Theory, and Matrices. These techniques are used by real program checkers.

arXiv++ Combinatorics

Proving programs terminate using well orderings, Ramsey Theory, and Matrices

Abstract

BibTeX