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.