Ph.D. in Computer Science. Sapienza, University of Rome, October 2013
Thesis: Verification of Artifact-centric Processes
Supervisor: Prof. G. De Giacomo
The focus of my dissertation was in formal methods and knowledge representation. In particular, I enabled the analysis and design of data-centric business workflows by developing frameworks and logics for structured data that are modified over time. I was also involved in EU-projects, teaching activities (software engineering course) and in the supervision of M.Sc. students.
M.Sc. in Computer Engineering. Sapienza, University of Rome, March 2009
Graduation Honors: Magna cum laude
Supervisor: Prof. G. De Giacomo
Specialization on artificial intelligence, top grade.
In my master thesis I devised a technique to automatically orchestrate public web services, allowing the synthesis of new services from a repository of existing ones. The thesis was published and presented at a flagship conference in AI.
B.Sc. in Computer Engineering. Sapienza, University of Rome, December 2006
Final Mark: Top grade
Work Experience
Principal Research Engineer - Collins Aerospace Applied Research and Technology. Cork, Ireland. From June 2023 to present.
Researcher - Uppsala University. Uppsala, Sweden. From October 2020 to October 2022
Research and development of SMT solvers for the theory of strings and regular expressions.
Postdoctoral Researcher - Stockholm University. Stockholm, Sweden. From November 2017 to October 2019
Department of Philosophy, supervisor: Prof. Valentin Goranko
I am investigating frameworks and formal reasoning techniques, in particular strategic reasoning, for dynamical multi- agents systems where not only agents are dynamical, e.g., change their states, but the systems themselves evolve by modifying their characteristic aspects, such as number and type of agents and their relationships.
Researcher - Bruno Kessler Foundation (FBK). Trento, Italy. From March 2014 to August 2017
In the PDI group, head: Dott.ssa Chiara Ghidini
My group focused on AI techniques for business process management, spanning from verification of workflows (to avoid errors at design phase) to the automated generation of models from activity logs (for auditing purposes).
I extended the investigation towards data-centric models and incorporated authorisation constraints by establishing a collaboration with the Security and Trust group.
Participating in a EU-project, as well as mentoring and supervising international students during their internships/theses were also part of my daily routine.
Postdoctoral fellow - DIAG dept., Sapienza, University of Rome. Rome, Italy. From August 2013 to March 2014
Supervisor: Prof. Giuseppe De Giacomo
I studied the differences between the finite and infinite semantics of linear-time temporal logic with emphasis on runtime monitoring. I co-supervised some M.Sc. students.
Research fellow - UCSB. Santa Barbara, CA, USA. From June 2013 to August 2013
Supervisor: Prof. Jianwen Su
I studied data mappings and integration between different data schemas.
Research scholar - UCSB. Santa Barbara, CA, USA. From February 2012 to September 2012
Supervisor: Prof. Jianwen Su
I explored runtime verification of first-order temporal properties as an alternative way to model-checking business workflows. My approach exploited the idea of a monitor which observes the workflow evolution and stops their executions whenever the temporal specifications are violated.
Research Intern - IBM T. J. Watson Research Center. New York, NY, USA. From June 2010 to September 2010
Supervisor: Prof. Rick Hull
Companies are interested not only in formal verification of business workflows, but also in facilitating the process of designing them. I therefore assessed the quality of procedural and declarative models for a variety of real-word scenarios, from (structured) product manufacturing to (more loose) healthcare guidelines.
Research Interests
Multi-agent systems and strategic reasoning;
Propositional and first-order temporal logics, formal analysis, offline verification and runtime monitoring;
Business process models and data-aware approaches for modeling workflows;
Formal verification applied to security: satisfiability of workflows with authorization constraints.
Library for translating Linear-time Temporal Logic (LTL) and Linear Dynamic Logic (LDL) formulas with finite-trace semantics to automata, so as to perform satisfiability and validity reasoning tasks in the finite-trace setting (Java, 13K+ LOC);
Library for the translation of First-order Linear-time Temporal logic (FO-LTL) to automata, under finite-domain assumption (Java, 18K+ LOC);
A process model discovery which, from a log, returns a "fuzzy" Petri net representing the process (Java, 8K+ LOC).
Teaching
Software Engineering
I was the lecturer of the Software Engineering course at Sabina Universitas, Rieti, IT during term 2010-2011.
Interns Supervisor
I supervised several M.Sc. and B.Sc. students form both Sapienza and from University of Trento for their theses and internships at FBK.
Participation on Boards and Committees
PC member of IJCAI 2018 and 2019;
PC member of AAAI 2019;
PC co-chair of the Artificial Intelligence for BPM (AI4BPM) Workshop at BPM 2018;
Member of the organizing committee of the Business Process Innovation with Artificial Intelligence (BPAI) Workshop at BPM 2017;
PC member of the International Conference on Software and System Processes (ICSSP) 2017;
PC member of Special Session for CIDM: Process Mining of the IEEE Symposium Series on Computational Intelligence 2016.