Invited speakers

Prof. Flemming Nielson, Technical University of Denmark (DTU), Denmark

Prof. Luke Ong, Oxford University, UK

Prof. Joachim Parrow, Uppsala University, Sweden

Prof. Kaisa Sere, Åbo Akademi University, Finland


Flemming Nielson (joint work with Hanne Riis Nielson, Han Gao)
The CaPiTo Approach to Protocol Validation

We show how to model service-oriented applications using the process algebra CaPiTo so that, on the one hand, we can achieve an abstract specification without being overwhelmed by the underlying implementation details and, on the other hand, we can obtain a concrete specification respecting the industrial standards used for ensuring security. We consider this development important in order to get a good agreement between the protocols analysed by formal tools and the applications developed by practitioners. We then show how to transform the concrete specification into the LySa analysis framework, used in the SENSORIA EU project and originally developed in the DEGAS EU project, for analysing cryptographic protocols under a Dolev-Yao attacker. This allows us to perform a control flow analysis for ensuring the authenticity (as well as confidentiality) of messages exchanged between services. The LySa analysis framework is implemented in polynomial time in the size of the protocol specification using the Succinct Solver, that can solve a superset of Datalog clauses.
Download speech slides

Luke Ong
Recursion schemes and the model checking of higher-order functional programs

Recursion schemes are in essence the simply-typed lambda calculus with recursion, generated from uninterpreted first-order symbols. An old model of computation much studied in the 70's, there has been a revival of interest in recursion schemes as generators of rich infinite structures (such as infinite trees) for modelling higher-order computation. In this talk we will survey recent proofs of the decidability of monadic second order theories of these structures, discuss implementations of these algorithms, and applications to the model checking of higher-order functional programs.
Download speech slides

Joachim Parrow
Concurrency and Proofs

In the first part of this talk I shall outline a framework for high level descriptions of concurrent systems. One main point is that it is parametric: data structures and logics can be chosen to fit particular applications. In the second part I shall comment on our experiences in using a theorem prover to establish the framework: not only does it provide us with complete certainty, it also promotes good proof structures and a flexible and general environment.

Kaisa Sere
Formal methods - from basic research to industrial deployment

In this talk we discuss a continuum of projects where methodological results within formal methods research have been systematically and gradually developed so that they have become mature enough for industrial use. We describe first the findings made in our research lab and thereafter show how these findings were applied in an "industry as lab" type of research project to industrial systems. We describe the interplay between the research at the lab and the more application oriented work. Finally, tool support was built and further co-operation with industrial partners is used to gather evidence of the impact of the methods in current industrial system development practice. The research decribed in this talk has been carried out within three consequtive EU funded projects (FP5 Matisse, FP6 Rodin, FP7 Deploy) during 2000-10.
Download speech slides


Conference Images added. (15.11.2010)
Registration closed. (28.09.2010)
Registration opened. (27.09.2010)
Sponsors added. (20.08.2010)
Call for Papers added. (05.07.2010)