mefisto logo

Mefisto Home | Mefisto@Venice | Participants in Venice | Publications | Documentation | Tools | Events

Overall of the Project:

The project aims at studying the theoretical foundations for the analysis and design of secure systems, with particular care to communication protocols for distributed systems.
In particular, the primary goal of the project is the development of techniques and methodologies for the analysys and verification of secure systems, to be used in the design process. Particular emphasis will be devoted to static analysis techniques (such as type systems, control flow analyses and abstract interpretation) and to dynamic or behavioural techniques (such as equvalence checking and model checking). The plan also includes the development of prototypal, automatic or semi-automatic verification tools based on these techniques.

Objectives of the Venice Team:

The research team of this unit is characterized by a solid experience in the fields of security, dynamic/behavioural verification of security properties, abstract interpretation, semantics-based program manipulation and verification, type theory and type systems. We expect that the cross-fertilization of these different backgrounds will lead to significant scientific contributions in the area of formal methods for security. Many security properties proposed will be approached through different static analysis techniques, namely abstract interpretation, proof methods and type systems.

Further Information about Mefisto project:

Partners: