Proving Program Termination With Matrix Weighted Digraphs

Abstract

Program termination analysis is an important task in logic and computer science. While determining if a program terminates is known to be undecidable in general, there has been a significant amount of attention given to finding sufficient and computationally practical conditions to prove termination. One such method takes a program and builds from it a matrix weighted digraph. These are directed graphs whose edges are labeled by square matrices with entries in {-1,0,1}, equipped with a nonstandard matrix multiplication. Certain properties of this digraph are known to imply the termination of the related program. In particular, termination of the program can be determined from the weights of the circuits in the digraph. In this talk, the motivation for addressing termination and how matrix weighted digraphs arise will be briefly discussed. The remainder of the talk will describe an efficient method for bounding the weights of a finite set of the circuits in a matrix weighted digraph, which allows termination of the related program to be deduced.