Linear-relations analysis of transition systems discovers linear invariant relationships among the variables of the system. These relationships help establish important safety and liveness properties. Efficient techniques for the analysis of systems using polyhedra have been explored, leading to the development of successful tools like HyTech. However, existing techniques rely on the use of approximations such as widening and extrapolation in order to ensure termination. In an earlier paper, we demonstrated the use of Farkas Lemma to provide a translation from the linear-relations analysis problem into a system of constraints on the unknown coefficients of a candidate invariant. However, since the constraints in question are non-linear, a naive application of the method does not scale. In this paper, we show that by some efficient simplifications and approximations to the quantifier elimination procedure, not only does the method scale to higher dimensions, but also enjoys performance advantages for some larger examples
In Static Analysis Symposium (SAS 2004).
Our prototype analyzer available here .
© 2004, Springer Verlag