Research Activities

The Systems Security Modelling and Analysis (SySMA) unit at IMT Lucca deals with the development of languages and techniques for the analysis, evaluation and verification of possibly distributed systems. The SySMA unit goal is to push the use of formal methods as methodological and automatic tools for the development of high-quality, correct software and systems that are secure, fast, usable, reusable, maintainable, and modular. We also study algorithms and systems to protect the security and integrity of computer systems, the information they store, and the people who use them. We make large usage of formal methods as enabling technology also for the security-by-design development model.

To make the developed tools usable by programmers not acquainted with the underlying mathematical foundations, SySMA aims at useful and effective but disappearing formal methods. Main areas of expertise are concurrency theory, programming languages, and software engineering, cybersecurity with a wide range of applications to adaptive systems, cyber-physical systems, cloud computing, computational biology, fake news, fault-tolerant systems and transportation networks.

SySMA participates in national and international projects and organizes conferences and workshops in the research fields of interest. We are also part of C3T, the Tuscan Cybersecurity Competence Center that carries out research and technology transfer activities in the field of information security to inform, raise awareness and respond to the needs of small and medium-sized enterprises, public bodies and professionals in relation to cybersecurity threats.

Our main areas of expertise are concurrency theory, programming languages, and software engineering, with a wide range of applications such as adaptive systems, cyber-physical systems, cloud computing, computational biology, fault-tolerant systems, security and transportation networks. Specific topics include:

System Modeling

Markov chains; Differential equations; Abstraction Techniques.

Software Engineering

Domain Specific Languages; Software Performance; Software Product Lin...

System Verification

Temporal Logics; Model Checking; Type Systems.

Cybersecurity

Cyber-Range; Malware Analysis; Network Security; Security o...

Social Impact

Security Awareness; Fake News; Blockchain and Smart Contracts.