[cs at parma seminars] Poliedri convessi per l'analisi e la verifica di sistemi hardware e software

[Roberto Bagnara]

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

POLIEDRI CONVESSI PER L'ANALISI E LA VERIFICA DI SISTEMI HARDWARE E SOFTWARE
============================================================================

                          CICLO DI SEMINARI
                          -----------------

             http://www.cs.unipr.it/ppl/seminars_2003_2004
             ---------------------------------------------

Come annunciato in precedenza, il giorno 26 febbraio 2004 si terra`,
presso il Dipartimento di Matematica dell'Universita` di Parma, il
terzo e ultimo gruppo di seminari nell'ambito del ciclo sui poliedri
convessi e le loro applicazioni nel campo dell'analisi e della
verifica di sistemi hardware e software.  I seminari avranno luogo
secondo il seguente calendario (i primi 6 seminari si sono tenuti il
18 e 19 novembre e il 10 e 11 dicembre 2003).
Per ulteriori informazioni e aggiornamenti si rimanda alla pagina
http://www.cs.unipr.it/ppl/seminars_2003_2004

7) February 26th, 2004, 14:30
    Roberto Bagnara, Dipartimento di Matematica, University of Parma, Italy
    Representation and Manipulation of Not Necessarily Closed Convex Polyhedra

8) February 26th, 2004, 15:45
    Enea Zaffanella, Dipartimento di Matematica, University of Parma, Italy
    Widenings for Powerset Domains with Applications to
    Finite Sets of Polyhedra

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

Date:     Thursday, February 26, 2004

Time:     14:30

Speaker:  Roberto Bagnara
           Dipartimento di Matematica, University of Parma, Italy

Title:    Representation and Manipulation of Not Necessarily Closed
           Convex Polyhedra

Abstract: Convex polyhedra, commonly employed for the analysis and
           verification of both hardware and software, may be defined
           either by a finite set of linear inequality constraints or
           by finite sets of generating points and rays of the
           polyhedron.  Although most implementations of the polyhedral
           operations assume that the polyhedra are topologically
           closed (i.e., all the constraints defining them are
           non-strict), several analyzers and verifiers need to compute
           on a domain of convex polyhedra that are not necessarily
           closed (NNC).  We propose a generalization of the well-known
           theorems by Minkowski and Weyl, where the concept of
           generator of an NNC polyhedron is extended to also account
           for the closure points of the polyhedron.  In particular, we
           show that any NNC polyhedron can be defined directly by
           means of an extended generator system, namely, a triple of
           finite sets containing rays, points and closure points of
           the polyhedron.  We propose two alternative implementations
           for NNC polyhedra, discussing the relative benefits and how
           the choice of representation can affect the efficiency of
           the polyhedral operations.  We also provide a novel solution
           to the issue of providing a non-redundant description of NNC
           polyhedra.

Place:    Sala Riunioni
           Department of Mathematics
           University of Parma
           Via D'Azeglio, 85/A
           Parma, Italy

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

Date:     Thursday, February 26, 2004

Time:     15:45

Speaker:  Enea Zaffanella
           Dipartimento di Matematica, University of Parma, Italy

Title:    Widenings for Powerset Domains with Applications to
           Finite Sets of Polyhedra

Abstract: The finite powerset construction upgrades an abstract domain
           by allowing for the representation of finite disjunctions of
           its elements.  In this talk we present three generic widening
           operators for the finite powerset abstract domain. All
           widenings are obtained by lifting any widening operator
           defined on the base-level abstract domain and are parametric
           with respect to the specification of a few additional
           operators.  We illustrate the proposed techniques by
           instantiating our widenings on powersets of convex
           polyhedra, a domain for which no non-trivial widening
           operator was previously known.

Place:    Sala Riunioni
           Department of Mathematics
           University of Parma
           Via D'Azeglio, 85/A
           Parma, Italy

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

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