CS Seminar: David Merchat, May 24, 2005

Speaker

Dr. David Merchat,
VERIMAG-IMAG
Gières, France.

Date and Time

Tuesday, May 24, 2005 at 16:00

Place

Sala Riunioni,
Dipartimento di Matematica, Università di Parma, I-43100 Parma

Title

Reducing the number of numerical variables in linear relations analysis

Abstract

The seminar describes research work done in the field of automatic verification of numerical properties, mainly for embedded systems. During verification one must represent, in a finite way, the possibly infinite set of values that a tuple of program variables can take. The domain of convex polyhedra offers one possible solution to this problem. This representation is precise but expensive, so that the number of program variables one can simultaneously approximate is limited. The goal of the research we present is to increase the maximum number of variables that it is possible to represent without incurring excessive computational costs. Two approaches have been considered and tested. First we wanted to benefit from the presence of linear equations in order to eliminate variables from the representation (as values for these variables could be recovered by means of the equations). Experimentation showed that this approach does not perform well in practice. Another approach, more promising, is the use of the cartesian product. The idea is to represent independently the variables whose evolution is not dependent. This decomposition can be improved through a change of basis. We will discuss the experimental results obtained with an analyser we developed in order to test these two approaches.

Contact Person

Roberto Bagnara

[Page last updated on May 23, 2005, 08:53:47.]