Faculty Profile

Prof. Spalazzi is working, since a long time, on formal methods applied to software engineering and computer and network security. He has provided an original contribution on defining the Semantic Model Checking, a tool for the formal verification of semantically annotated processes. Regarding the application of formal methods to software engineering, he has worked on the application of semantic model checking to service computing. More in depth, he has cooperated with IRST-FBK (Trento, Italy) and University of Brescia (Italy) on semantic service identification, selection, and composition. He has also applied formal methods on agent-oriented software engineering. More in depth, he has cooperated with SRI International (Menlo Park, California) and University of Toronto (Canada) at a development environment based on Tropos. Regarding the application of formal methods to security, he has worked on formal verification of security protocols and grid job scheduling.

Luca Spalazzi is an associate professor at the Università Politecnica delle Marche, Italy. He received the M.S. in Electronic Engineering and the Ph.D. in Artificial Intelligent Systems from the University of Ancona, Italy in 1989 and 1994, respectively. He has worked as consultant at the Istituto di Ricerca Scientifica e Tecnologica (IRST), Trento, Italy (1991–1997). He was a visiting scholar at the Australian Artificial Intelligence Institute (AAII), Carlton, Vic., Australia and at the Computer Science Department, Stanford University, California in 1992 and 1996, respectively. His research has been supported by grants from European Union and Italian Minister of University and Scientific Research. His present research areas include Formal Methods and Model Checking applied to Semantic Web Services, Computer and Network Security (in cooperation with Italian State Police), and Multi-agent Systems.