About myself
From November, 2025, I am working as the Head of Strategic Initiatives within Eolo, one of the largest Fixed Wireless Access (FWA) Internet service providers in the world.
On the 28th of March, 2026, I obtained my Executive Master in Business Administration from SDA Bocconi, Milan, Italy.
From April, 2022, since October, 2025, I have been heading the Network Engineering department of Eolo. Within my mandate I have defined and executed the EOLO's technology-driven growth strategy, enabling the world's first commercial 5G SA mmWave-only FWA network and repositioning the company toward higher-value customer segments.
From September, 2018, since April, 2022, I have been leading the R&D department of Eolo, in charge of designing and evolving all network software systems of EOLO, with a strong focus on networking automation solutions.
From June, 2016, since August, 2018, I have been working as a software engineer in Eolo, contributing to the BLU project, the Eolo SDN framework.
From February, 2015, since May, 2016, I have been working as a researcher at the San Raffaele Scientific Institute. My activity at the San Raffaele Scientific Institute was focused on the design and development of frameworks for processing genomic data stemming from high-throughput sequencing technologies, such as NGS.
On the 17th of February, 2015, I defended my PhD thesis titled "An SMT-based verification framework for software systems handling arrays" (available here).
From September, 2010, since January, 2015 I have been working as a Research Assistant in the Formal verification group of the Università della Svizzera Italiana led by Prof. Natasha Sharygina.
In 2014 I have been awarded a research fellowship from the SNSF (Doc.Mobility program) giving me the great opportunity of joining Prof. David Monniaux's group at Verimag for six months (from January to June, 2014).
In 2010 I have been working for three months (June - August) as a research intern at FBK in the "Security & Trust" unit led by Prof. Alessandro Armando.
On the 26th of April, 2010, I got my M.Sc. degree in Computer Science from the Università degli Studi di Milano (University of Milan, Italy) with a thesis (available here in Italian language only) on the formal parameterized verification of fault-tolerant protocols.
On the 25th October, 2007, I got my B.Sc. degree in Computer Science from the Università degli Studi di Milano (University of Milan, Italy) with a thesis (available here in Italian language only) on the analysis of stop condition approaches for epidemic algorithms used in opportunistic networks.
Most relevant projects I have been working on
-
BLU
The EOLO SDN framework. More details about BLU are available here. -
Booster
An abstraction and acceleration-based software model-checker for programs handling arrays. More details about Booster are available here. -
Automated Support for the Design and Validation of Parameterized Systems
Towards the application of infinite-state model checkers in the design and verification of fault-tolerant parameterized protocols. More details about this project are available here. -
MCMT
A model checker for infinite-state systems based on the integration of Satisfiability Modulo Theories (SMT) solving and backward reachability. More details about MCMT are available here.
Publications
Show all 24 publications (2010–2017)
- 24. "Cardinality constraints for arrays (decidability results and applications)" [Link]
- 23. "A framework for the verification of parameterized infinite-state systems" [Link]
- 22. "Counting Constraints in Flat Array Fragments" [Link]
- 21. "Counter Abstractions in Model Checking of Distributed Broadcast Algorithms: Some Case Studies" [Link]
- 20. "A new Acceleration-based Combination Framework for Array Properties" [Link]
- 19. "A simple abstraction of arrays and maps by program translation" [Link]
- 18. "Decision Procedures for Flat Array Properties" [Link]
- 17. "Polyhedra to the rescue of array interpolants" [Link]
- 16. "Monotonic Abstraction Techniques: from Parametric to Software Model Checking" [Link]
- 15. "Booster: an acceleration-based verification framework for array programs" [Link]
- 14. "VERIGE: VERification with Invariant Generation Engine" [Link]
- 13. "A framework for the verification of parameterized infinite-state systems" [Link]
- 12. "An extension of Lazy Abstraction with Interpolation for programs with arrays" [Link]
- 11. "Decision Procedures for Flat Array Properties" [Link] [Slides]
- 10. "Acceleration-based Safety Decision Procedure for Programs with Arrays" [Link] [Slides]
- 9. "Definability of Accelerated Relations in a Theory of Arrays and its Applications" [Link] [Slides]
- 8. "SAFARI: SMT-based Abstraction For Arrays with Interpolants" [Link]
- 7. "Reachability Modulo Theory Library" [Link]
- 6. "Lazy Abstraction with Interpolants for Arrays" [Link] [Slides]
- 5. "Universal guards, relativization of quantifiers, and failure models in model checking modulo theories" [Link]
- 4. "ASASP: Automated Symbolic Analysis of Security Policies" [Link]
- 3. "Efficient Symbolic Automated Analysis of Administrative Attribute-based RBAC-policies" [Link]
- 2. "Automated Support for the Design and Validation of Parameterized Systems: a case study" [Link] [Slides]
- 1. "Brief Announcement: Automated Support for the Design and Validation of Parameterized Systems: a case study" [Link]
Teaching
Show teaching activity (2010–2017)
- Lecturer for the course "Introduction to C programming", part of the course "Metodi e tecniche per lo sviluppo Cloud" ("Methods and technologies for cloud developers"), organized by ITS INCOM Foundation, 2017.
- Teaching assistant for the course "Discrete Mathematics" (USI), academic year 2014/15 - Fall semester.
- Teaching assistant for the course "Automata and Formal Languages" (USI), academic year 2012/13 - Spring semester.
- Teaching assistant for the course "Software Atelier V: Languages and Compilers" (USI), academic year 2012/13 - Fall semester.
- Teaching assistant for the course "Automata and Formal Languages" (USI), academic year 2011/12 - Spring semester.
- Teaching assistant for the course "Theory of Computation" (USI), academic year 2011/12 - Fall semester.
- Teaching assistant for the course "Software Atelier I: Software Tools" (USI), academic year 2010/11 - Fall semester.