Proving programs terminate using well orderings, Ramsey Theory, and Matrices
classification
🧮 math.CO
cs.LO
keywords
programterminatesuserdatainputmatricesorderingsprograms
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.