Massimo Bartoletti

Massimo Bartoletti is Associate Professor at the Department of Mathematics and Computer Science of the University of Cagliari. He got a PhD in Computer Science at the University of Pisa in 2005. 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 coordinates the node of the Cyber Security National Lab at the Department of Mathematics and Computer Science of the University of Cagliari, and the Blockchain@Unica research lab. He is editor-in-chief of the "Non-financial Blockchains" section of Frontiers in Blockchain. He is external consultant of Extus.

He is, or he has been, scientific coordinator of the following research projects:

  • RAS LR7/07 TESLA "Enforcement Techniques for the Security of Languages and Applications"
  • RAS LR7/07 TRICS "A Trusted Reservation Infrastructure for Computational Societies",
  • PIA 2010 Social Glue (co-coordinator with Salvatore Carta)
  • PRIN 2010-11 Security Horizons (local coordinator for Unica)
  • PIA 2013 NOMAD (co-coordinator with Salvatore Carta)
  • RAS 2017 SCORE "Smart COllaboRative Engineering"

Massimo Bartoletti published over fifty research papers on refereed journals and international refereed conferences and workshops. He served as program committee member and organizer for international conferences and workshops (e.g. SAC, WS-FM, ICE, WWV, FCS-ARSPA, ARES, AINA, TGC, FAST, BYTECODE, WTSC, CILC, SERIAL, CryBlock, Euro-Par, BCRB, WETSEB, SerCo, IWBOSE) and external reviewer for several journals and international conferences. He has served as chair for ICE 2016, SOAP 2017, ICE 2017, CIBB 2017, SOAP 2018, ICE 2018. He is member of the scientific committee of the Scientific School on Blockchain & Distributed Ledger Technology, and member of the steering committee of the Distributed Ledger Technology Workshop.

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).