Personale docente

Roberto Bagnara began his training in Computer Science at the University of Bologna (May 1984 - December 1987) and Geneva's CERN, where he worked in the group of Tim Berners-Lee, inventor of the World Wide Web (January 1988 - July 1989). He received a laurea degree (magna cum laude, July 1992) and a Ph.D. (September 1997), both in Computer Science, from the University of Pisa. He has been Research Fellow at the School of Computer Studies of the University of Leeds (January-October 1997) and Assistant Professor at the University of Parma (November 1997 - December 2001), Associate Professor of Computer Science at the same university (December 2001 -October 2010) where he is now Full Professor of Computer Science (since November 2010). He has been Visiting Researcher/Professor at Monash University, Melbourne (January-February 1995), the University of La Réunion (various periods from 2002 to 2010) and École Polytechnique, Paris (June-July 2008).

Since 2000 he is a member of the Board of Professors of the Ph.D. School on Mathematics and Statistics for the Computational Sciences of the University of Milan and, since 1997, he teaches university courses at all levels on the foundations of computer science, programming languages, advanced programming techniques, software analysis and verification. He has supervised numerous laurea theses and has been member of national and European Ph.D. committees.

He is active, since 20 years, in the fields of abstract interpretation, program analysis and verification, and semantics-based program manipulation.

Abstract interpretation is a theory of approximation of discrete systems conceived at the end of the 1970s by Patrick and Radhia Cousot, France. This theory allows to formally specify provably correct approximation processes for the behavior of any computing system. For example, abstract interpretation provides methods that are general enough to specify static program analyzers, automatic verifiers of software and hardware systems, automatic verifiers of the properties of communication protocols, type systems and so forth. The abstract interpretation research field is extremely lively: the International Static Analysis Symposium (SAS) and the International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI) are the annual conferences dedicated to this sector, but numerous contributions are presented also at the International Conference on Computer Aided Verification (CAV), ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) and other conferences/symposia. There is a significant research community, especially in Europe (and in Italy, in particular, as witnessed by numerous PRIN projects on abstract interpretation or related themes), in the United States and in Asia. Abstract interpretation is having a considerable industrial impact due to the inescapable necessity of guaranteeing the quality of safety critical software. For example, the PolySpace static analyzer, which works on C, C++ and Ada programs, was conceived and entirely designed by means of abstract interpretation and it is a product quite successfully commercialized by the multinational company TheMathWorks. The Microsoft Visual Studio development environment includes a module for the static analysis of .NET bytecode for the automatic inference of correctness specifications (the so-called Code Contracts). Finally, but this list could continue, we can mention the ASTRÉE static analyzer, developed by the research team of Patrick and Radhia Cousot, which is commercialized by the German company AbsInt and used by the Airbus consortium for the certification of safety critical on-board software for the Airbus A340 e A380 airplanes.

Roberto Bagnara has coauthored around 40 papers on the above mentioned topics that have been published in international journals and proceedings of international conferences with referees. In particular, the results achieved together with his coauthors concern: logic and constraint logic programming both as the object and as an instrument for program analysis and verification;

• the use in abstract interpretation of constraint propagation techniques previously confined to the field of artificial intelligence;
  
• variable aliasing and sharing in logic programming;
  
• the simplification for the analysis of pair-sharing of the domain of Jacobs and Langen;
  
• the generalization of this domain to the case where the occur-check is not performed, its combination with domains tracking variable freeness and linearity, the definition of widening operators over such combined domains in order to accelerate convergence of the analysis;
  
• the decomposition of abstract domains by means of quotients and complementation;
  
• the analysis of term structure in constraint logic programs, with or without the occur-check;
  
• the first finiteness analysis for (constraint) logic programs based on the theory of rational trees;
  
• the generalization to not necessarily closed convex polyhedra of the double description method (introduced by Motzkin et al.), in a way that is completely independent from the particular implementation technique;
  
• the generalization of the technique by Halbwachs et al. for the implementation of not necessarily closed convex polyhedra based on epsilon-representations;
  
• the definition of a general framework for the definition of new widening operators on the domain of convex polyhedra (generalizable to other domains), whereby one or more approximation heuristics can be systematically turned into widening operators that are more precise of the standard widening of Cousot and Halbwachs; before this work, and for 25 years, the standard widening was the only known widening operator over the domain of convex polyhedra;
  
• the introduction of techniques for the "lifting" of widening operators to abstract domains obtained by means of the finite powerset construction (which allows to represent all the finite disjunctions of a given abstract domain);
  
• the solution of the problems caused by the "syntactic" definition of weakly relational domains (such as systems of bounded differences and the so-called "octagons") obtained by adopting "semantic" definitions that are exempt from redundancies and from convergence problems and, at the same time, allow for intuitive interfaces;
  
• new abstract domains for the generation of invariants expressed by conjunctions of polynomial inequalities (of bounded degree) or by sets of points and hyperplanes linearly distributed over an n-dimensional vector space (rational grids);
  
• a new, cubic algorithm for the entailment closure of a set of integer "octagonal" constraints (previously known algorithms are both asymptotically more complex and less efficient even on small instances);
  
• the definition of a framework for abstract-interpretation-based static analysis of imperative languages, such as C, C++ and Java, that supports relational domains as well as pointers, compound data objects and non-structured control-flow mechanisms.
  

The research of Roberto Bagnara joins a scrupulous investigation on the theoretical foundations with the experimental validation and application to concrete contexts. He has been the inspiration for and the principal architect of several software projects in the above mentioned research domains, including the Parma Polyhedra Library (PPL), a library of numerical abstractions especially targeted at applications in the field of analysis and verification of hardware and software systems. The PPL is used in numerous projects at the most prestigious research centers and, in particular, it is employed in GCC (GNU Compiler Collection, the compilers' suite most used worldwide). He is the main author of China, a state-of-the-art data-flow analyzer for constraint logic programs (http://www.cs.unipr.it/China/). He also led the PURRS project (Parma University's Recurrence Relation Solver, http://www.cs.unipr.it/purrs/). He is now leading the ECLAIR project, an industrial-strength platform for the analysis, verification and transformation for imperative languages: C, C++ and Java to start with.

Roberto Bagnara has been a member of program committees for international conferences and symposia, among which the already mentioned SAS and VMCAI, Annual ACM Symposium on Applied Computing (SAC, Technical Track on Software Verification), International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), International Conference on Logic Programming (ICLP). He has also organized international workshops and summer schools and he has been invited to speak at international workshops and research centers. He regularly acts as a referee for the main international journals, conferences and symposia concerning his research interests.

He has participated in several international and national research projects: ESPRIT Basic Research Action Project n. 6707 ("ParForce"); COFIN'99 MURST project "Automatic Program Certification by Abstract Interpretation"; COFIN'00 MURST project "Abstract Interpretation, Type Systems and Control-Flow Analysis"; COFIN'01 MURST project "Aggregate- and Number-Reasoning for Computing".

He was responsible for the Parma research unit in national projects PRIN'02 MURST project "Constraint Based Verification of Reactive Systems"; PRIN'04 MURST project "AIDA - Abstract Interpretation Design and Applications"; PRIN'07 MURST project "AIDA2007 - Abstract Interpretation Design and Applications." He was the Italian coordinator for the Italy-Spain bilateral project "Advanced Development Environment for Logic Programs" (IT229, 2001-2002). He also led the Parma unit in the project GlobalGCC (GGCC, 2006-2009), a project belonging to the ITEA program (Information Technology for European Advancement) devoted to the introduction, in the GNU Compiler Collection, of global analysis techniques.

Roberto Bagnara is also Chief Scientist and President of BUGSENG srl, a spin-off company of the University of Parma, whose mission is the transfer of sofisticate software verification and validation technologies into industry.

A much more detailed CV is available at http://www.cs.unipr.it/~bagnara/