PRL Seminars

The SUP-INF algorithm is essentially a symbolic linear programming algorithm that is used by many automated and interactive theorem provers as the main step in a heuristic to verify linear inequalities over the integers.

Although the algorithm has been in use since at least the mid 1970s, there are reasons to believe that the treatments it has received in the literature are not sufficient to prove its correctness. For example, the only published proof that the algorithm terminates is incorrect, and recent examples indicate that the algorithm can be sensitive to the order of summands in arithmetic expressions, highlighting the importance of details previously omitted or treated vaguely.

In this talk, we outline our work in progress on giving a formal account of the SUP-INF algorithm and a proof of its correctness. Our account is based on an axiomatic description of a collection of abstract data types that express, in an economical way, the data structure and operational requirements of the algorithm and place a minimum of restrictions on how the algorithm is implemented. These ADTs are specified in a subset of the Extended ML specification language (with an additional provision for defining nondeterministic or nonextensional operations), for which we outline a type-theoretic semantics.

We also outline the direction the formal proof of correctness will take. The formalization raises several issues concerning the role of behavioral equivalence and nondeterminism in program specification, which we may also address if there is time.