Abstract thinking is a chore for many - for me, on good days, a feast and a joy.
Nietzsche, Unveroffentlichtes aus der Umwerthungszeit 1882/88
Research interests
I am mostly interested in abstract interpretation and approximation methods with applications in any area of computer science, from semantics to static program analysis, software and hardware verification, model-checking and abstract model-checking, program transformation and optimization, software watermarking and code obfuscation, complexity and computability, logic and constraint-based programming, computer virology, security and safety critical systems. Recently I am more and more interested in foundational aspects of computation, with particular attention to the relation between intensional and extensional properties of code. Abstract interpretation is the perfect formal setting to understand this duality. I am also interested inapplying these methods in security, digital asset protection, and in malware analysis, as well as in all fields of CS where approximation methds can be useful. In all these fields I am interested in studying systematic methods for approximating undecidable or highly complex problems by means of formal methods such as abstract interpretation. I believe that abstract interpretation represents a unifying theory for understanding most phenomena connected with computation. In pure math I am interested in lattice theory and closure systems.
Short CV
Roberto Giacobazzi was born in 1964 in Modena, Italy. He received the Laurea degree in Computer Science in 1988 from the University of Pisa, and in 1993 he received the Ph.D. in Computer Science from the same university, with a Ph.D. thesis on Semantic aspects of logic program analysis, under the supervision of Prof. Giorgio Levi. From 1993 to 1995 he had a Post Doctoral Research position at Laboratoire d'Informatique (LIX), Ecole Polytechnique (Paris) in the equipe of Patrick and Radhia Cousot. From 1995 to 1998 he was (tenured) Assistant Professor in Computer Science at the University of Pisa. From 1998 to 2000 he was Associate Professor at the University of Verona. From May 2000 until September 2023 he is Full Professor in Computer Science at the University of Verona. From October 2023 he is Full Professor in Computer Science at the U. of Arizona. He has been visiting professor at The Ben Gurion University of Negev, KAIST Institute of Technology, Ecole Polytechnique (Paris), Ecole Normale Superieure (Paris), IRDETO Corp., The University of Melbourne, The University of Louisiana at Lafayette, The IMDEA SW Institute, the Universidad Complutense de Madrid, and the University of Hawaii at Manoa. He is the Scientific Leader of the SPY-Lab and co-founder of Julia, Vero4Chain and Cytherel. From October 2006 until October 2012 he was the Dean of the College of Science of the University of Verona, and from 2018 to 2022 was Head of the Department of Computer Science of the University of Verona. The research interests of Roberto Giacobazzi include abstract interpretation, static program analysis, semantics of programming languages, program verification, abstract model-checking, program transformation and optimization, digital asset protection, code obfuscation, software watermarking, computability, and lattice theory. He is author of more than 100 publications in international journals and conferences and he is involved in national (Italian) and international (European) research projects in the field of static program analysis. His main current research interest is in formal methods for systematic design of domains and transfer functions for abstract interpretation, with application in security, digital asset protection, code obfuscation, watermarking, malware analysis, semantics, program analysis, computability, and abstract model-checking. In the past, he gave a declarative semantics for Prolog control features and he studied new methodologies to design static program analyzers and optimization techniques for logic and constraint-based languages by abstract interpretation. In lattice theory he contributed to understanding of the structure of the lattice of closure operators and complete congruence relations on complete lattices. He was in the Steering Committee of the Static Analysis Symposium (SAS) and of the ACM Conference on Principles of Programming Languages (POPL).
