[cs at parma seminars] Poliedri convessi per l'analisi e la verifica di sistemi hardware e software
Roberto Bagnara
bagnara at cs.unipr.it
Tue Nov 4 17:06:34 CET 2003
[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
---------------------------------------------
Nei prossimi mesi si terra`, presso il Dipartimento di Matematica
dell'Universita` di Parma, un ciclo di seminari 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. Per ulteriori informazioni e aggiornamenti
si rimanda alla pagina http://www.cs.unipr.it/ppl/seminars_2003_2004
1) November 18th, 2003, 14:30
Fabio Torrisi, ETH Zurich, Switzerland
Convexity Recognition of the Union of Polyhedra
2) November 18th, 2003, 15:45
Fabio Torrisi, ETH Zurich, Switzerland
Inner and Outer Approximations of Polytopes Using Boxes
3) November 19th, 2003, 14:30
Patricia M. Hill, School of Computing, University of Leeds, UK
Discrete Numerical Domains for the Analysis of Software
4) December 10th, 2003, 14:30
Fausto Spoto, Dipartimento di Informatica, University of Verona, Italy
JULIA: A Static Analyser for the Java Bytecode
5) December 11th, 2003, 14:30
Roberto Bagnara, Dipartimento di Matematica, University of Parma, Italy
Convex Polyhedra for the Analysis and Verification of Hardware
and Software Systems: the "Parma Polyhedra Library"
6) December 11th, 2003, 15:45
Enea Zaffanella, Dipartimento di Matematica, University of Parma, Italy
New Widening Operators for Convex Polyhedra
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: Tuesday, November 18th, 2003
Time: 14:30
Speaker: Fabio Torrisi
ETH Zurich, Switzerland
Title: Convexity Recognition of the Union of Polyhedra
Abstract: In this talk, we consider the following basic problem in
polyhedral computation: Given two polyhedra in finite
dimension, P and Q, decide whether their union is convex,
and, if so, compute it. We consider the three natural
specializations of the problem: (1) when the polyhedra are
given by halfspaces (H-polyhedra), (2) when they are given
by vertices and extreme rays (V-polyhedra), and (3) when
both H- and V-polyhedral representations are available. Both
the bounded (polytopes) and the unbounded case are
considered. We show that the first two problems are
polynomially solvable, and that the third problem is
strongly-polynomially solvable.
Place: Sala Riunioni
Department of Mathematics
University of Parma
Via D'Azeglio, 85/A
Parma, Italy
======================================================================
Date: Tuesday, November 18th, 2003
Time: 15:45
Speaker: Fabio Torrisi
ETH Zurich, Switzerland
Title: Inner and Outer Approximations of Polytopes Using Boxes
Abstract: The talk deals with the problem of approximating a convex
polytope in any finite dimension by a collection of
(hyper)boxes. More exactly, given a polytope P by a system
of linear inequalities, we look for two collections I and E
of boxes with non-overlapping interiors such that the union
of all boxes in I is contained in P and the union of all
boxes in E contains P. We propose and test several
techniques to construct I and E aimed at getting a good
balance between two contrasting objectives: minimize the
volume error and minimize the total number of generated
boxes. We suggest how to modify the proposed techniques in
order to approximate the projection of P onto a given
subspace without computing the projection explicitly.
Place: Sala Riunioni
Department of Mathematics
University of Parma
Via D'Azeglio, 85/A
Parma, Italy
======================================================================
Date: Wednesday, November 19th, 2003
Time: 14:30
Speaker: Patricia M. Hill
School of Computing, University of Leeds, UK
Title: Discrete Numerical Domains for the Analysis of Software
Abstract: Many static analysis applications of polyhedra require
information on certain regularly spaced discrete values
such as those on an integer grid that occur within the
polyhedra. The domain of point lattices, being a
natural generalization of the set of integral points in
an n-dimensional space, is an appropriate domain for
representing the discrete values. In this talk we will
describe this domain, its two representations that mirror
the constraint and generator descriptions for convex
polyhedra, and several operations required for their use
with polyhedra in static analysis.
Place: Sala Riunioni
Department of Mathematics
University of Parma
Via D'Azeglio, 85/A
Parma, Italy
======================================================================
Date: Wednesday, December 10th, 2003
Time: 14:30
Speaker: Fausto Spoto
Dipartimento di Informatica, University of Verona, Italy
Title: JULIA: A Static Analyser for the Java Bytecode
Abstract: We describe our JULIA static analyser for the Java bytecode.
Its main feature is to analyse the Java bytecode directly,
without any previous transformation into a high-level
language such as Java. This improves the efficiency of the
analysis and yields an analysis which is insensitive to
possible errors of the transformation into Java. JULIA is
based on a denotational semantics for the Java bytecode,
focused on a set of program points called watchpoints. The
cost of the analysis is proportional to the number of
watchpoints. An abstract domain for Java is a class
implementing the abstract counterparts of the Java
bytecodes. We show some examples of abstract domains for
class and escape analysis. We show that the traditional
technique of abstract compilation has major effects on the
efficiency of the analysis. Finally, we discuss the
possibility of developing an abstract domain for
approximating numerical variables, which is useful to remove
array checks. This domain should be based on the Parma
Polyhedra Library.
Place: Sala Riunioni
Department of Mathematics
University of Parma
Via D'Azeglio, 85/A
Parma, Italy
======================================================================
Date: Thursday, December 11th, 2003
Time: 14:30
Speaker: Roberto Bagnara
Dipartimento di Matematica, University of Parma, Italy
Title: Convex Polyhedra for the Analysis and Verification of Hardware
and Software Systems: the "Parma Polyhedra Library"
Abstract: The domain of convex polyhedra is employed in several
systems for the analysis and verification of hardware and
software components. Current applications span imperative,
functional and logic languages, synchronous languages and
synchronization protocols, real-time and hybrid systems.
Since the seminal work of P. Cousot and N. Halbwachs, convex
polyhedra have thus played an important role in the formal
methods community and several critical tasks rely on their
software implementations. Despite this, existing libraries
for the manipulation of convex polyhedra are still research
prototypes and suffer from limitations that make their usage
problematic, especially in critical applications. In this
talk we present the "Parma Polyhedra Library", a new, robust
and complete implementation of convex polyhedra,
concentrating on the distinctive features of the library,
the novel theoretical underpinnings and the future
development directions.
Place: Sala Riunioni
Department of Mathematics
University of Parma
Via D'Azeglio, 85/A
Parma, Italy
======================================================================
Date: Thursday, December 11th, 2003
Time: 15:45
Speaker: Enea Zaffanella
Dipartimento di Matematica, University of Parma, Italy
Title: New Widening Operators for Convex Polyhedra.
Abstract: In the Abstract Interpretation framework, widening operators
provide a simple and general mechanisms for enforcing and
accelerating the convergence of fixpoint computations.
For the domain of convex polyhedra, the original widening
operator proposed by Cousot and Halbwachs amply deserves the
name of standard widening since most analysis and
verification tools that employ convex polyhedra also employ
that operator. Nonetheless, there is an unfulfilled demand
for more precise widening operators. In this talk we
introduce the standard widening and we present a framework
for the systematic definition of new widening operators
improving on it. The framework is then instantiated so as to
obtain a new widening operator that combines several
heuristics and uses the standard widening as a last resort
so that it is never less precise.
Place: Sala Riunioni
Department of Mathematics
University of Parma
Via D'Azeglio, 85/A
Parma, Italy
======================================================================
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
More information about the Seminars
mailing list