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
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.
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.
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.
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.
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)
|Email: nwpt10 (at) abo.fi, Phone: +358 2 215 4754, Fax: +358 2 215 4732|