[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
----------------------------------------------------------------------