cs@parma

Home

People

Projects

Publications

Seminars

Software

Links

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

Page maintained by
Enea Zaffanella

Home | People | Projects | Publications | Seminars | Software | Links