
CS Seminar: Enric RodríguezCarbonell, January 11, 2005
 Speaker

Dr. Enric
RodríguezCarbonell,
Departament de Llenguatges i Sistemes
Informàtics (LSI),
Technical University of Catalonia (UPC),
Barcelona, Spain.
 Date and Time

Tuesday, January 11, 2005 at 14:30
 Place

Sala Riunioni,
Dipartimento di Matematica,
Università di Parma,
Via D'Azeglio 85/A,
I43100 Parma
 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.
 Slides

Generation of Polynomial Equality Invariants by Abstract Interpretation (pdf, 158 kB).
 Contact Person

Roberto Bagnara
[Page last updated on January 21, 2013, 08:18:53.]
