Proving programs terminate using well orderings, Ramsey Theory, and Matrices
From MaRDI portal
Publication:6227151
arXiv1108.3347MaRDI QIDQ6227151FDOQ6227151
Authors: William Gasarch 
Publication date: 16 August 2011
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.
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Ramsey theory (05D10) Second- and higher-order arithmetic and fragments (03F35)
This page was built for publication: Proving programs terminate using well orderings, Ramsey Theory, and Matrices
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6227151)
