Modern society is increasingly dependent on complex software systems involving large numbers of heterogeneous, autonomous components interconnected by networks with dynamic topologies. As these systems provide access to fundamental services, their correctness and reliability is becoming a prominent aspect of everyday life. And yet, their design and deployment pose unprecedented challenges, mostly because they must account for unforeseen changes and evolutions of the environment in which they execute. Because of their complex and dynamic nature, classical formal methods for software development, analysis and verification are not yet able to provide sufficiently strong guarantees on the correctness and reliability of such systems. This calls for a new generation of formal methods to assist software developers. Types are a flexible and expressive way of specifying and analyzing software properties and the ongoing research on type systems shows that their full potential is yet to be fully uncovered.
The goal of the "Dynamically and Autonomously Reconfigurable Types" (DART) project is to propose a new comprehensive view of types to face the new challenges of programming autonomic and distributed systems, providing at the same time:
- 1) formal theories defining new type systems,
- 2) effective analysis techniques based on these type systems and
- 3) tools for program specification and verification.
Torino group
- Luca Padovani, PRINCIPAL INVESTIGATOR
- Mario Coppo
- Mariangiola Dezani
- Viviana Bono
- Ugo de'Liguoro
- Sara Capecchi
Novi Sad group
- Jovanka Pantovic, PRINCIPAL INVESTIGATOR
- Silvia Ghilezan
- Jelena Ivetic
- Svetlana Jaksic, PhD student
- Jelena Colic, Phd student
- Jovana Radenovic, PhD student
- Jovana Obradovic, PhD student