Since April, 2022, I am the Head of Network Engineering department of Eolo, one of the largest Fixed Wireless Access (FWA) Internet service providers in the world.
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.
24. |
"Cardinality constraints for arrays (decidability results and applications)"
Formal Methods in System Design (FMSD), vol. 51, p. 545-574, 2017
[Link]
|
---|---|
23. |
"A framework for the verification of parameterized infinite-state systems"
Fundamenta Informaticae, vol. 150, no. 1, p. 1-24, 2017
[Link]
|
22. |
"Counting Constraints in Flat Array Fragments"
Automated Reasoning - 8th International Joint Conference (IJCAR), Coimbra, Portugal, June 27 - July 2, 2016
[Link]
|
21. |
"Counter Abstractions in Model Checking of Distributed Broadcast Algorithms: Some Case Studies"
31st Italian Conference on Computational Logic (CILC), Milan, Italy, June 20-22, 2016
[Link]
|
20. |
"A new Acceleration-based Combination Framework for Array Properties"
10th International Symposium on Frontiers of Combining Systems (FroCoS), Wrocław, Poland, September 19-24, 2015
[Link]
|
19. |
"A simple abstraction of arrays and maps by program translation"
22nd International Static Analysis Symposium (SAS), Saint-Malo, France, September 9-11, 2015
[Link]
|
18. |
"Decision Procedures for Flat Array Properties"
Journal of Automated Reasoning (JAR), vol. 54, p. 327-352, 2015
[Link]
|
17. |
"Polyhedra to the rescue of array interpolants"
30th ACM/SIGAPP Symposium On Applied Computing (SAC), Salamanca, Spain, April 13-17, 2015
[Link]
|
16. |
"Monotonic Abstraction Techniques: from Parametric to Software Model Checking"
1st Workshop on Logics and Model-checking for Self-* Systems (MOD*), UITP 2014, Bertinoro, Italy, September 12, 2014
[Link]
|
15. |
"Booster: an acceleration-based verification framework for array programs"
12th International Symposium on Automated Technology for Verification and Analysis (ATVA), Sydney, Australia, November 3-7, 2014
[Link]
|
14. |
"VERIGE: VERification with Invariant Generation Engine"
21st International Symposium on Model Checking of Software (SPIN), San Josè, California, USA, July 21-23, 2014
[Link]
|
13. |
"A framework for the verification of parameterized infinite-state systems"
29th Italian Conference on Computational Logic (CILC), Turin, Italy, June 16-18, 2014
[Link]
|
12. |
"An extension of Lazy Abstraction with Interpolation for programs with arrays"
Formal Methods in System Design (FMSD), vol. 45, p. 63-109, 2014
[Link]
|
11. |
"Decision Procedures for Flat Array Properties"
20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Grenoble, France, April 5-13, 2014
|
10. |
"Acceleration-based Safety Decision Procedure for Programs with Arrays"
Short paper at the 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Stellenbosh, South Africa, December 15-19, 2013.
|
9. |
"Definability of Accelerated Relations in a Theory of Arrays and its Applications"
9th International Symposium on Frontiers of Combining Systems (FroCoS), Nancy, France, September 18-20, 2013.
|
8. |
"SAFARI: SMT-based Abstraction For Arrays with Interpolants"
24th International Conference on Computer Aided Verification (CAV), Berkeley, California, USA, July 7-13, 2012.
[Link]
|
7. |
"Reachability Modulo Theory Library"
10th International Workshop on Satisfiability Modulo Theories (SMT), Manchester, UK, June 30 - July 1, 2012.
[Link]
|
6. |
"Lazy Abstraction with Interpolants for Arrays"
18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Mérida, Venezuela, March 10-15, 2012.
|
5. |
"Universal guards, relativization of quantifiers, and failure models in model checking modulo theories"
Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 8, p. 29-61, 2012
[Link]
|
4. |
"ASASP: Automated Symbolic Analysis of Security Policies"
23rd International Conference on Automated Deduction (CADE), Wrocław, Poland, July 31 - August 5, 2011.
[Link]
|
3. |
"Efficient Symbolic Automated Analysis of Administrative Attribute-based RBAC-policies"
6th ACM Symposium on Information, Computer and Communications Security (ASIACCS), Hong Kong, March 22-24, 2011.
[Link]
|
2. |
"Automated Support for the Design and Validation of Parameterized Systems: a case study"
10th International Workshop on Automated Verification of Critical Systems (AVoCS), Dusseldorf, Germany, September 21-23, 2010.
Electronic Communications of the EASST (ECEASST), vol 35, 2010.
|
1. |
"Brief Announcement: Automated Support for the Design and Validation of Parameterized Systems: a case study"
XXIV DIStributed Computing Conference (DISC), Boston, Massachusetts, USA, September 13-15, 2010.
[Link]
|