[PPL-devel] Seminario

[Roberto Bagnara]

[Con preghiera di diffusione e scuse per l'eventuale ricezione di copie
multiple.  RB]


----------------------------------------------------------------------

Date:     Martedi`, 24 maggio 2005

Time:     16:00

Speaker:  David Merchat
           VERIMAG-IMAG
           GIÈRES, Francia

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 approximated 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.

Place:    Sala Riunioni
           Dipartimento di Matematica
           Universita` di Parma
           Parco Area delle Scienze, 53/A
           Parma

----------------------------------------------------------------------

-- 
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it