Software verification based on linear programming

Abstract

We introduce a new software verification method based on plain linear programming. The problematic is being given a software S and a property P, to find whether there exists a path (i.e. a test sequence) of S satisfying P, or a proof that P is impossible to satisfy. The software S is modelized as a set of communicating automata which in turn is translated into a system of linear equations in positive numbers. Property P is then translated as extra linear equations added to this system. We define the extended notion of flow-path (which includes the notion of path) permitting the automata to carry flows of data rather than undividable tokens. By applying linear programming in a sophisticated way to the linear system, it is possible, in time polynomial in the size of (S, P), either to display a flow-path of S satisfying P or to prove that P is impossible to satisfy. The existence of a flow-path does not always imply the existence of a path, as it can be non-integer valued. Yet, on all our modelized examples, the study of the flow-path solution always permitted either to display a path satisfying P or to underscore a reason proving P to be impossible to satisfy. The first part of this document introduces the theoretical background of our method. The second part sums up results of the use of our method on some systems of industrial size.