The research activity of Massimo Bartoletti focuses on formal methods for the specification, analysis and verification of software and systems, on security, on impure functional languages, on concurrency theory, on the semantics of programming languages, on theories of contracts, and on logics for the specification and verification of properties of software and systems.
In particular, he developed control flow analyses, type and effect systems, and model-checking algorithms as a support for the definition of security models for programming languages. On such basis, he implemented and optimized security mechanisms for object-oriented languages like Java. The static analysis techniques developed in such studies have been extended to design Web service infrastructures guaranteeing that the orchestration of services is correct with respect to the security constraints imposed by the programmer.
Recently, Massimo Bartoletti has investigated the theoretical foundations upon which constructing service infrastructures where clients and services have provable guarantees about their mutual behaviour. One of the key ideas is that the interaction between services and their clients have to be regulated by suitable contracts, through which one can specify the desired and the offered properties. Such contracts should not only have a legal value: they must also have a formal one. Contracts have to be mathematical entities, which allow for precisely establishing the rights and the duties of clients and services, as well as the sanctions which have to be imposed in case they are violated. These studies have led to a new paradigm for the invocation of services, named "call-by-contract", which allows clients to specify the semantic properties that have to be enjoyed by the invoked service.
Massimo Bartoletti participated in national research projects (PRIN Project Mefisto “Formal Methods for Security and Time”, PRIN Project Sybilla “Systems Biology: modelling, languages, analysis”, PRIN Project Soft “Security-Oriented Formal Techniques”), as well as international ones (EU-FET Global Computing Project IST-2001-32072 Degas “Design Environments for Global Applications”, EU-FETPI Global Computing Project IST-2005-16004 Sensoria “Software Engineering for Service-Oriented Overlay Computers”, COST Action IC1201 BETTY “Behavioural types for Reliable Large-Scale Software Systems”). He is coordinator of the node of the Cyber Security National Lab at the Department of Mathematics and Computer Science of the University of Cagliari.
He is, or he has been, scientific coordinator of the following research projects:
Massimo Bartoletti taught/teaches undergraduate and PhD courses in Programming Languages, Computer Architecture, Theoretical Computer Science, Security Foundations, Calculi and Models for Security. Some of his work has been subject of monographic courses at international PhD schools, e.g. "Foundations of Security Analysis and Design" (FOSAD 2006), "Advanced applications of model-checking techniques" (SEFM School 2010), "Behavioural contracts" (BETTY Summer School 2016).