Skip to Main Content
Advances in Computers
book

Advances in Computers

by Atif Memon
February 2015
Intermediate to advanced content levelIntermediate to advanced
276 pages
7h 8m
English
Academic Press
Content preview from Advances in Computers
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 ...

Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.
Start your free trial

You might also like

Advances in Computers

Advances in Computers

Atif Memon

Publisher Resources

ISBN: 9780128021330