Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
SAS04: Abstract for Paper 59
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, not only does the method scale to higher
dimensions, but also enjoys performance advantages
for some larger examples.