 | |
All
sessions take place in auditorium 8.| 09:00- | 09:45
| Joost-Pieter Katoen, U
Twente, The Netherlands
Invited
talk: Model checking birth and death
In
this talk we propose Allocational Temporal Logic (AllTL) as a
formalism to express properties concerning the dynamic allocation (birth)
and de-allocation (death) of entities, such as the objects in an
object-based system. The logic is interpreted on History-Dependent B"uchi
Automata, extended with a symbolic representation for certain cases of
unbounded allocation. We also present a simple imperative language with
primitive statements for (de)allocation, and provide it with a finite-state
operational semantics, to demonstrate the kind of behaviour that can be
modelled. The main result that we will present is a tableau-based
model-checking algorithm for AllTL, along the lines of Lichtenstein and
Pnueli's algorithm for LTL. (This is aj oint work with Dino Distefano and
Arend Rensink.) |
| 09:45- | 10:30
| Natasha Sharygina, U Texas-Austin, USA
James
C. Browne, U Texas-Austin, USA
Model
checking large-scale software via abstraction of loop
transitions
This
paper outlines an on-going project on the abstract data
model checking of large-scale programs. The focus of the paper is the data
abstraction algorithm that is targeted to minimize the contribution of the
loop executions to the program state space. The loop abstraction is defined
as the syntactic program transformation that results in the sound
representation of the concrete program. We demonstrate the loop abstraction
algorithm in the context of the integrated software design and
model-checking. |
| 11:00- | 11:45
| Alessandro Armando, U Genova, Italy
Pasquale
De Lucia, U Genova, Italy
Symbolic
model-checking of linear programs
A
fundamental problem in the development of model-checking
techniques for sequential programs is the identification of models
(analogous to the finite state machines used for modeling hardware
circuits) for which reasonably simple abstractions from conventional
programming languages (such as C and Java) as well as efficient
model-checking procedures do exist. Previous work developed at Microsoft
Research proposed boolean programs as a model for sequential programs and a
model-checking procedure for this family of programs. In this paper we
build on top and extend on these ideas and propose linear programs as an
alternative model for sequential programs. We argue that linear programs
offer a better model in many cases as they provide a level of abstraction
closer to programs arising in many practical situations. We show how a
model-checking procedure for linear programs can be built on top of a
constraint solver for linear arithmetics and present some experimental
results obtained with our prototype implementation of the
model-checker. |
| 11:45- | 12:30
| Pierluigi Ammirati, U Genova, Italy
Giorgio
Delzanno, U Genova, Italy
Pierre
Ganty, U Brussels (Libre), Belgium
Gilles
Geeraerts, U Brussels (Libre), Belgium
Jean-François
Raskin, U Brussels (Libre), Belgium
Laurent
Van Begin, U Brussels (Libre), Belgium
Babylon:
An integrated toolkit for the specification and
verification of parameterized systems |
| 14:00- | 14:45
| Alessandro Armando, U Genova, Italy
Invited
talk: An overview of the AVISS project
This
1 year assessment project aims at laying the foundations of
a new generation of verification tools for automatic error detection for
e-commerce and related security protocols. To assess the potential of this
technology, we will develop a prototype verification tool incorporating
inference engines based on three promising automated deduction techniques:
on-the-fly model-checking based on lazy data-types, theorem-proving with
constraints, and model-checking based on propositional satisfiability
checking. |
| 14:45- | 15:30
| Benjamin Aziz, Dublin City U, Ireland
G.
W. Hamilton, Dublin City U, Ireland
A
privacy analysis for the π-calculus: The denotational approach
We
present a non-uniform static analysis for the π-calculus that is
built on a denotational
semantics of the language and is useful in detecting instances of
information leakage and insecure communications in mobile systems with
multi-level security policies. To ensure the termination of the analysis,
we propose a safe abstraction, which ensures a finite number of names are
generated by any process. We also describe a tool called Picasso that
implements the analysis. |
| 16:00- | 16:45
| Fabio Martinelli, CNR Pisa, Italy
Symbolic
partial model checking for security analysis |
| 16:45- | 17:30
| R. Corin, U Twente, The Netherlands
Sandro
Etalle, U Twente, The Netherlands
An
improved constraint-based system for the verification of security
protocols |
|
|