I’m currently a postdoctoral research fellow at the Computer Science department of the University of Milan (Italy), where I teach software engineering, and I work in the software engineering research group. During my Ph.D. program, I have been selected to participate at the ACM Student Research Competition and Doctoral Symposium of different editions of the ICSE conference. I received my PhD degree in Computer Science from the University of Milan in 2014. My dissertation focused on the combination of advanced abstraction techniques and big data approaches to tackle the state explosion problem in formal verification. My current research activity focuses on Formal Methods and Software Engineering. I’m especially interested in: uncertainty quantification in software development; model-based testing techniques; methods and tools to improve dependability of adaptable and evolvable time-dependent applications. If you want more information about me, you can take a look at my complete Curriculum Vitae (last update: Feb. 2019).
3rd Int. Workshop on Formal Approaches for Advanced Computing Systems (FAACS) 2019. In Organizing Committee. TBA.
4th Int. Workshop on Microservices: Science and Engineering (MSE) 2019. In PC. Submission.
9th Int. Conference on Cloud Computing and Services Science (CLOSER) 2019. In PC. Submission.
This section contains my latest news about research and teaching activities.
The paper "A High-level Petri Net-based Formal Model of Distributed Self-adaptive Systems" has been accepted for presentation at the 2nd International Workshop on Formal Approaches For Advanced Computing Systems (FAACS @ ECSA 2018).
The paper "Online Model-based testing Under Uncertainty" has been accepted for presentation at the 29th IEEE International Symposium on Software Reliability Engineering (ISSRE 2018).
The manuscript "Zone-based formal specification and timing analysis of real-time self-adaptive systems" is currently in press in the Elsevier Science of Computer Programming journal.
The paper "Towards Evolving Petri Nets: a Symmetric Nets Based Framework" has been accepted for presentation at the 14th International Workshop on Discrete Event Systems (WODES 2018).
The paper "Design-time to Run-time Verification of Microservices Based Applications" has been accepted for presentation at the 1st International Workshop on Formal Approaches for Advanced Computing Systems (FAACS 2017).
The paper "A Formal Framework for Specifying and Verifying Microservices Based Process Flows" has been accepted for presentation at the 2nd International Workshop on Microservices: Science and Engineering (MSE@SEFM 2017).
The paper "Towards Inverse Uncertainty Quantification in Software Development" has been accepted for presentation at the 15th International Conference on Software Engineering and Formal Methods (SEFM 2017).
The paper Event-based Runtime Verification of Temporal Properties using Time Basic Petri Nets has been accepted for presentation at the 9th NASA Formal Methods Symposium NFM 2017.
My main research interests cover the macro-areas of Software Engineering, formal methods and formal Verification with particular focus to methods and tools to improve dependability of time-dependent, adaptable and evolvable applications.
A list of my research papers can be obtained from different sources reported below.
The Uncertainty-aware MBT module is a software tool that implements a (on-the-fly) MBT algorithm that takes explicitely into account the uncertainty specified by the tester in order to deliver high confidence in the software product out from the testing activity.
PNemu is an extensible Python library that provides all the necessary to model/verify Self-Adaptive Systems using High-Level Petri nets (HLPNs).
The MahaRAJA framework is a event-based runtime verification software tool for verifying at runtime the relationship among events and their temporal properties on Java programs.
The ZAFETY framework is a Zone-based approach to specify and verify real-time self-adaptive systems. It relies on a particular modeling technique based on timed extensions of Petri nets. The framework allows the verification of (timed) robustness properties to guarantee self-healing capabilities when higher levels of reliability and availability are required.
Mardigras is a distributed graph building framework able to cope with the State-space explosion problem. The framework is a powerful tool for constructing high-performance distributed applications without the need for the user to care about every non-functional aspects through an easy-to-understand abstraction for programmers.
Graphgen is a software tool for state space analysis of Time-Basic (TB) Petri nets. It builds a symbolic reachability graph relying on a time coverage analysis approach.
Requirements analysis and architecture design of the Smart Breack Project, in collaboration with Bialetti Industrie S.p.a.
This section contains my current and past teaching activities. Past teaching activities: refer to this old web page.
Corso di laurea triennale in Informatica. Dipartimento di informatica,Università degli Studi di Milano.