With his PhD-Thesis’ work Alessandro Gianola had already won the 2022 Best Italian PhD Thesis in Theoretical Computer Science award, given by the Italian Chapter of the European Association for Theoretical Computer Science (EATCS), and the 2022 Best BPM Dissertation award, given by the BPM Association at the 20th International Conference on Business Process Management (BPM 2022).  

The CADE Bill McCune PhD Award is a recognition established by 2019 CADE Inc. to honour each year a PhD thesis defended the previous year, for its substantive contributions to the field of Automated Reasoning, its theory, its implementation, and/or its application on important problems. Named after the American computer scientist William Walker McCune, this award is highly regarded by the international Automated Reasoning community. 

Gianola’s winning thesis, titled “SMT-based Safety Verification of Data-Aware Processes: Foundations and Applications," was supervised by Prof. Marco Montali of unibz and Prof. Silvio Ghilardi from the Università degli Studi di Milano. The thesis delves into the development of logical-mathematical methods, particularly model-theoretical approaches, to tackle verification problems in systems with infinite states. These methods hold significant applications in the domain of business process management (BPM), making them valuable tools for ensuring the safety and correctness of complex processes involving data. 

The motivation behind awarding Gianola’s thesis lay in its groundbreaking contributions to Automated Reasoning: “It introduces a comprehensive framework for automating safety verification of processes and data, laying the groundwork for the integration and extension of infinite-state model checkers. These developments enable successful and scalable verification of data-aware processes, with implications beyond their immediate applications. Notably, Gianola’s thesis also presented pioneering theoretical results on model completion and uniform interpolation for Satisfiability Modulo Theories (SMT) and their combinations, extending the frontiers of knowledge in the field”. 

Gianola’s work is divided into two main parts. The first one is dedicated to theoretical, foundational aspects, emphasizing the best AI and automated reasoning techniques for studying the behaviour of dynamic and complex systems in companies and organizations that involve interactions between processes and data. This included the analysis of so-called “infinite-state systems”, where it is impractical to examine all possible outcomes exhaustively. Instead, symbolic techniques were employed to analyze these infinite configurations efficiently. The second part of the thesis focused on applying these broad techniques to real-world contexts in business process management. Gianola developed concrete algorithms for analyzing process safety, evaluating whether the defined processes could reach or not undesirable or unwanted states. 

Commenting on the significance of his research, Gianola explained: “The objective of my research is to find methods that can determine whether these systems operate correctly, fulfilling their intended purposes and identifying potential errors or flaws that may lead to hazardous configurations”.  

Alessandro Gianola’s research forms part of a broader project, where both theoretical and practical advancements in artificial intelligence techniques are pursued. The ultimate goal is to develop innovative algorithmic implementations with potential real-world applications in the industry. Thus, his achievements not only enrich the scientific community but also hold promise for solving real-world challenges in various domains. 

(zil)