SAVE on Saturday

Detailed program
Saturday July 27th, 2002
See also the unified by-slot program

All sessions take place in auditorium 8.

Session 1

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.

Session 2

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

Session 3

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.

Session 4

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