[cs at parma seminars] Due seminari sulla generazione e le applicazioni di invarianti polinomiali

[Roberto Bagnara]

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


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

Date:     Martedi`, 11 gennaio 2005

Time:     14:30

Speaker:  Enric Rodriguez Carbonell
           Technical University of Catalonia (UPC)
           Barcelona, Spain

Title:    Generation of Polynomial Equality Invariants by Abstract
           Interpretation

Abstract: Program verification aims at proving that a program meets its
           specification, i.e. that the actual program behaviour
           coincides with the desired one. Invariants are properties
           that hold at any reachable state of the system, and are
           essential in order to prove safety requirements, when one
           must show that the system will never reach a bad
           state. Abstract interpretation is a framework for generating
           these invariants, which can be expressed in a variety of
           languages, e.g. intervals, linear inequalities and modular
           equalities.  This seminar is focused on finding polynomial
           equality invariants by means of the abstract interpretation
           approach. The semantics of a simple imperative programming
           language is given in terms of ideals of polynomials, a basic
           concept in algebraic geometry. It is shown with some
           examples how polynomial invariants can be employed in order
           to verify properties of imperative programs.

Place:    Sala Riunioni
           Dipartimento di Matematica
           Universita` di Parma
           Via D'Azeglio, 85/A
           Parma

======================================================================

Date:     Martedi`, 11 gennaio 2005

Time:     15:45

Speaker:  Enric Rodriguez Carbonell
           Technical University of Catalonia (UPC)
           Barcelona, Spain

Title:    Applications of Polynomial Invariants

Abstract: In a previous talk, the application of polynomial invariants
           to the verification of imperative programs has been
           discussed. In this seminar it is shown how polynomial
           invariants can also be employed in order to verify
           properties of other classes of systems: Petri nets and
           hybrid systems.  Petri nets are a mathematical modelling
           tool for studying systems that are characterized as being
           concurrent, asynchronous, distributed, parallel,
           non-deterministic, and/or stochastic.  On the other hand,
           hybrid systems are systems that have discrete event dynamics
           as well as continuous time dynamics. They are used in the
           analysis of, e.g, continuous systems with phased operations
           (walking robots, biological cell growth and division) and
           continuous systems controlled by discrete logic (aircraft
           autopilot modes, thermostats, chemical plants with valves
           and pumps, automobile automatic transmissions).

Place:    Sala Riunioni
           Dipartimento di Matematica
           Universita` di Parma
           Via D'Azeglio, 85/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