[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 Dec 9 10:40:40 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
---------------------------------------------
Come annunciato in precedenza, nei giorni 10 e 11 dicembre 2003 si terra`,
presso il Dipartimento di Matematica dell'Universita` di Parma, il secondo
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 tre seminari si sono tenuti il 18 e 19 novembre 2003).
Per ulteriori informazioni e aggiornamenti si rimanda alla pagina
http://www.cs.unipr.it/ppl/seminars_2003_2004
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: 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