1. General information
• Full professor in Computer Science (“Informatica”, SSD INF/01) at the Dipartimento di Statistica, Informatica, Applicazioni (Department of Statistics, Informatics, Applications, DiSIA).
• Contacts:– Office: Dipartimento di Sistemi e Informatica Università di Firenze, Viale Morgagni 65 - I-50134, Firenze. Phone: +39 055 4237453.– E-mail: michele.boreale@unifi.it.– Web: www.dsi.unifi.it/~boreale/.
2. Research interestsThe research activity of Michele Boreale is centered around formal methods for the verification and specification of concurrent systems, in a broad sense including distributed systems, communication and security protocols. An important tool in this area is represented by process calculi, languages equipped with a rigorous semantics, which allow for compositional system descriptions, possibly at different levels of abstractions. As an example, process calculi can be employed to prove an implementation correctwith respect to a given specification. This can be done by relating system descriptions at different levels, via so-called behavioural relation, such as bisimulation, and the related proof and (automatic) verification techniques.In the problems considered by Boreale, the stress is on dynamicity, asynchrony and security of communications. The most significant results obtained by Boreale can be grouped in three broad topics, as follows.
• Semantics of process calculi, with an emphasis on the description of systems featuring dynamic generation and passing of references (channels), such as Milner’s pi-calculus.
• Languages and methods for analysing distributed and service-oriented applications. Process calculi scc and Caspis, and the related behavioural type systems, developed within the EU Sensoria project1, are outcomes of this research.
• Models and (quantitative) methods for the analysis of security protocols and systems, such as symbolic protocol analysis and quantitative information flow.
• Safety and invariants of dynamical systems.
3. Publications
https://dblp.org/pid/b/MBoreale.html
Legenda