|
CS Seminar: Enric Rodríguez-Carbonell, January 11, 2005
- Speaker
-
Dr. Enric
Rodríguez-Carbonell,
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,
I-43100 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.]
|