The summer school presented different methodologies for the specification
and the analysis of software systems.
About 70 graduate students, most of which west and east european, attended
the school.
Some mechanical techniques for the verification of systems have been
presented:
in particular, O. Grumberg and A. Pnueli presented model checking techniques,
while J. R. Abrial presented the proving strategies embedded in the Predicate
Prover integrated within the B-Method.
Other lectures introduced formal methods for system design:
P. Zave presented an integrated technique (Promela+Z) to deal with
the specification and verification of telecommunication services;
M. Abadi showed us his "spi-calculus", an enhancement of the pi-calculus for the analysis of security features of systems.
R. Kurki-Suonio lectures focussed on a TLA-based approach for the specification
of object systems while K. Sere presented Actions Systems.
R. Back and E. Hehner introduced programming logic and refinement methods.
We had two panel sessions in which the lectures could clarify some issues ontheir methodologies.
I met there young researchers with whom I discuss some topics: in particular
a participant who works at Nokia; we discussed some issues on mobility
and she told me about the interest topics at Nokia.