Gianola carried out his Ph.D. thesis, entitled “SMT-based Safety Verification of Data-Aware Processes: Foundations and Applications”, under the supervision of Prof. Marco Montali and the co-supervision of Prof. Silvio Ghilardi from Università degli Studi di Milano. The researcher used his strong background in mathematical logic and automated reasoning gained in his degree in Mathematics to obtain breakthroughs in business process management and artificial intelligence.

The first award won by Gianola was given by the Italian Chapter of the European Association for Theoretical Computer Science (EATCS). The award was presented at ICTCS 2022 in Rome, recognizing the groundbreaking contributions of the thesis to the theoretical investigation of the challenging problem of verifying infinite-state systems. The second award is an international one, the 2022 Best BPM Dissertation Award. The award was presented at the 20th International Conference on Business Process Management (BPM 2022) in Münster, Germany. The evaluation committee indicated Alessandro's thesis as a "magnum opus that considerably advances our understanding of data-aware business processes”. Notably, these prizes also come with the possibility of publishing a Springer monograph based on the results contained in the thesis.

But that’s not all. In addition, two publications related to Alessandro's thesis won two Best Paper awards: one for a work on SMT-based verification of multi-agent systems at the 23nd International Conference on Principles and Practice of Multi-Agent Systems (PRIMA 2020) and the other for a work on the use of SMT-based techniques for performing data-aware process mining tasks at the 19th International Conference on Business Process Management (BPM 2021).

“All in all, these awards witness the excellence of Alessandro's research. His contribution is further strengthening unibz as one of the most well-recognized research spots on the foundations of business process management and artificial intelligence. Most notably, these results contributed to advancing the state of the art not only on the problem of analyzing data-aware processes but also in general on the field of automated reasoning and artificial intelligence”, says Prof. Marco Montali.

More specifically, in his Ph.D. thesis he studied the problem of representing, in a machine-interpretable way, business processes in their full complexity. Business processes are employed in contemporary organizations and institutions to regulate how internal work is conducted to satisfy the needs of external customers and create value. To ensure that processes are well-defined and cannot lead to undesired outcomes, it is essential to equip information systems with the ability to automatically verify the correctness of processes before they are actually put into execution. This, however, poses a number of challenges. Traditionally, processes are described by focusing only on the flows of activities (for example the possible flows to manage customer orders in an order-to-delivery process), while neglecting the data manipulated during the process (such as the amount of money associated with customer orders and the type of customer), how activities manipulate this data, and how decisions use these data to determine how to route the process.

The first result obtained by Alessandro has been to formally capture this data-process interplay using a logic-based approach, connecting such formal representation to languages used by end-users (such as BPMN and SQL). Analyzing data-aware processes is extremely challenging, as this requires, in principle, to check infinitely many possible executions of the processes, with infinitely many configurations for the data (e.g., all the possible ways in which all possible customer orders may be managed).

This is where Alessandro obtained the most important results: the development of novel techniques from artificial intelligence and formal verification, where an intelligent software program can analyze a process of interest and check its correctness with a provably correct verdict, by abstractly reasoning on the possible process executions without exploring them one by one (which would be simply impossible, as they are infinitely many). Instead of developing ad-hoc algorithms to solve this problem, he shows how industrial-strength technologies can be effectively employed for the purpose of creating a bridge between theory and practice.