[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

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