|
Questo terzo workshop segue quello di Bologna, tenutosi il 13 febbraio 2003
presso il Dipartimento di Scienze dell'Informazione, e quello di Firenze
tenutosi il 25 e 26 settembre 2003 presso il Dipartimento di Sistemi
e Informatica.
La partecipazione è aperta a tutti gli interessati e, in special
modo, ai partecipanti al
CILC 2004.
Chi intende partecipare anche al pranzo
è bene lo faccia sapere per tempo.
Il workshop è organizzato da
Roberto Bagnara:
non esitate a scrivere
per ogni eventuale necessità.
Programma del workshop
| 10:30 |
Abstract Interpretation Against Races
Roberto Barbuti, Stefano Cataudella, Luca Tesei
Abstract.
In this paper we investigate the use of abstract interpretation
techniques for statically preventing race conditions. To this purpose we
enrich the concurrent object calculus concsigma by
annotating terms with the set of ``locks'' owned at any time. We use an
abstract form of the object calculus to check the absence of race
conditions. We show that abstract interpretation is more flexible than
type analyses, and it allows to certify as ``race free'' a larger class
of programs.
|
| 11:00 |
Generalizing the Paige-Tarjan Refinement Algorithm
through Abstract Interpretation
Francesco Ranzato, Francesco Tapparo
|
| 11:30 |
Pausa caffè |
| 11:45 |
Proving Abstract Non-Interference
Roberto Giacobazzi, Isabella Mastroeni
Abstract.
In this talk we introduce a compositional proof-system for certifying
abstract non-interference in programming languages. Certifying
abstract non-interference means proving that no unauthorized flow of
information is observable by the attacker from confidential to public
data. The properties of the computation that an attacker may observe
are specified in an abstract domain. Assertions specify the secrecy of
a program relatively to the given attacker and the proof-system
specifies how these assertions can be composed in a syntax-directed a
la Hoare deduction of secrecy. We prove that the proof-system is sound
relatively to the standard semantics of an imperative programming
languag. This provides a sound proof-system for both certifying
secrecy in language-based security and deriving attackers which do not
violate secrecy inductively on program's syntax.
|
| 12:15 |
Witness and Counterexample Automata
Alessandro Fantechi, Stefania Gnesi, Robert Meolic
Abstract.
Witnesses and counterexamples produced by model checkers provide a
very useful source of diagnostic information. They are usually
returned in the form of a single computation path along the model
of the system. However, a single computation path is not enough to
explain all reasons of a validity or a failure. Our work in this
area is motivated by the application of action-based model
checking algorithms to the test case generation for models
formally specified with a CCS-like process algebra. There, only
linear and finite witnesses and counterexamples are useful and for
the given formula and model an efficient representation of the set
of witnesses (counterexamples) explaining all reasons of validity
(failure) is needed. This paper identifies a fragment of action
computation tree logic (ACTL) that can be handled in this way.
Moreover, a suitable form of witnesses and counterexamples is
proposed and "witness" and "counterexample automata" are
introduced, which are finite automata recognizing them and an
algorithm for generating such automata is given.
|
| 13:00 |
Pausa pranzo
Zusmann's Rule:
A successful symposium depends on the ratio of meeting to eating.
Cucina parmigiana presso il Circolo Corale ``G. Verdi'',
Vicolo Asdente 9, Parma.
|
| 15:00 |
The Present and Future of the Parma Polyhedra Library:
Powersets, Octagons, Grids and Other Numerical Abstractions
Roberto Bagnara, Katy Dobson, Patricia M. Hill,
Elena Mazzi, Barbara Quartieri, Enea Zaffanella
Abstract.
The Parma Polyhedra Library is acknowledged to be a useful and
rather efficient software tool upon which further research work on
static analysis and abstract interpretation can be reliably based. In
this talk we present the current and future development of the Parma
Polyhedra Library, ranging from implementation improvements to more
fundamental research enhancements. In particular, we
distinguish between limit and distribution information about the
possible values of numerical variables. While limit information has
been extensively studied, distribution information is much less
popular and research work investigating their proper integration is
needed.
|
| 15:30 |
Precise Analysis of Pi-Calculus in Cubic Time
Gilberto Filé
|
| 16:00 |
Linear Constraints in Symbolic Software
Model Checking
Alessandro Armando, Cladio Castellini,
Jacopo Mantovani
Abstract.
Iterative abstraction refinement has emerged in the last few
years as a leading approach to software model checking. In this context
Boolean programs are commonly employed as simple, yet useful
abstractions from conventional programming languages. In this paper we
propose Linear Programs as a finer grained abstraction for sequential
programs and propose a model checking procedure for this family of
programs. We also present the EUREKA toolkit, which consists of a
prototype implementation of our model checking procedure for Linear
Programs as well as of a library of Linear Programs to be used for
benchmarking. Experimental results obtained by running our model
checker against the library provide evidence of the effectiveness of the
approach.
|
Hanno confermato la loro presenza:
Unità di Bologna
- Alessandro Fantechi
- Maurizio Gabbrielli
- Luca Tesei
Unità di Genova
- Alessandro Armando
- Jacopo Mantovani
Unità di Padova
- Gilberto Filé
- Francesco Ranzato
- Francesco Tapparo
Unità di Parma
- Roberto Bagnara
- Gianfranco Rossi
- Elio Panegai
- Enea Zaffanella
Unità di Udine
- Agostino Dovier
Unità di Verona
- Mila Dalla Preda
- Roberto Giacobazzi
- Isabella Mastroeni
- Giovanni Scardoni
- Roberto Segala
Visitatori (graditissimi)
- Roberta Gori
|
