Automatic synthesis of multiple ranking functions with supporting invariants via DISCOVERER

We present a new method for the generation of total degree ordering linear ranking functions supported by inductive linear invariants for loops with linear guards and transitions. Our method, based on Gordan´s Theorem, synthesizes linear ranking functions with supporting linear invariants over linear loops by extracting non-linear constraints on the coefficients of a predefined template from a program. The real algebraic tool DISCOVERER is utilized to solve these derived constraints. Two well-known programs are presented to demonstrate this technique. Moreover, our method is complete due to DISCOVERER.