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: