Associate Professor of Computer Engineering
Department of Engineering and Architecture, University of Trieste
I work on formal methods for the design and analysis of complex systems — cyber-physical and collective adaptive ones. My work spans spatio-temporal logics, scalable monitoring algorithms, and methods that learn temporal logic requirements directly from data.
My research is focused on formal methods applied to the design and analysis of complex systems, such as cyber-physical systems and collective adaptive systems. I develop frameworks to control and optimise their behaviour while keeping track of spatio-temporal dynamics: a spatio-temporal logic to express requirements on their performance, and scalable monitoring algorithms to verify them.
I am further interested in non-deterministic imprecision in spatio-temporal logics — both from samples and from parameter imprecision in formulas — and in discovering more precise, more expressive specifications. I also work on stochastic systems and statistical verification: a methodology for parameter estimation and synthesis that combines formal methods with machine learning, which can also learn temporal logic requirements from data, giving an automatic way to describe the behaviours a system must (or must not) satisfy.
full list → curriculum vitae · dblp
I supervise bachelor and master theses in Trieste. Most projects sit between formal methods and machine learning: you will write code, prove something, and see it run on real data. If one of these areas interests you — or you have your own idea — write to me and we will shape it together.