O'Reilly logo

Advances in Computers by Atif Memon

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

Chapter Four

Proving Programs Terminate Using Well-Founded Orderings, Ramsey's Theorem, and Matrices

William Gasarch    Department of Computer Science, University of Maryland, College Park, Maryland, USA

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 no matter what the user does. We define a program to terminate if no matter what the user does the program will halt.

We discuss various ways to prove that a program terminates. The proofs use well-founded orders, Ramsey Theorem, and matrices. These techniques are used by real program checkers.

General Terms

Verification

Theory

Keywords

Proving programs terminate ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required