Personale docente

Enea Zaffanella is Associate Professor in Computer Science at the University of Parma, since November 2006, working at the Department of Mathematics. Previously he has been Fellow Researcher (from June 2000 to December 2002) and Assistant Professor (from December 2002 to October 2006) at the same University. Since 2002 he teaches university courses for the degrees in Computer Science, Mathematics and Physics, ranging from programming methodologies (both at introductory and advanced levels), data base management systems and compilation of programming languages. He was a (co-) supervisor of several laurea theses focused on his research activity.

After obtaining a laurea degree in Computer Science from the University of Pisa in April 1993, he started his research activity at the Department of Computer Science of the University of Pisa. After a period working for the Universities of Modena and Parma, from 1997 to 2000, in 2002 he received the PhD in Computer Science from the School of Computing of the University of Leeds (UK), where later he has been a Visiting Researcher on several occasions.

The research activity, started early during the laurea thesis work, is focused on the field of static analysis and verification of software systems, based on Abstract Interpretation. In such a context, the relevant issues that are under investigation are connected to the specification of the semantics of programming languages, the development of formal techniques for the correct approximation of these semantics and, hence, the study, design, implementation and experimental evaluation of abstract domains and abstract operators supporting an effective automatic computation of these approximations. The research activity on these arguments lead to the joint publication of more than 35 papers appeared on international journals and proceedings of international conferences with referees.

A first part of the research results obtained is concerned with the analysis of (constraint) logic programs, possibly extended with constructs for the synchronization of concurrent processes. In such a context, one of the main topic of investigation was the study of abstract domains for the analysis of variable sharing: for this domain, besides providing a rigorous proof of correctness of the approximation, several modifications have been proposed that are able to improve the efficiency, the precision and the scalability of the resulting analysis, also in conjunction with other properties such as variable freeness, linearity and other structural information on logic terms. The results obtained are valid not only for the domain of finite trees, but also for the domain of rational trees and can be usefully applied in both contexts.

A second part of the research work is focused on the domains suitable for the approximation of the numerical quantities handled by programs. For the abstract domains of convex polyhedra, the double description method has been generalized to the case of polyhedra that are not necessarily closed, providing a justification of the correctness of the approach and a comparison of the intrinsic efficiency of alternative implementation schemes. For the class of weakly relational abstractions (systems of bounded differences and octagons) it was shown how a careful use of the closure by entailment and redundancy reduction operators allows for the specification of abstract domains that are based on the notion of semantic equivalence of representations, rather than a mere syntactic equivalence that was previously used. For the domain of octagons, a new closure by entailment operator was defined that is simpler and, at the same time, significantly more efficient than that previously known; also, new operators for the reduction of redundancies have been proposed, both for the rational and the integer cases. The investigation on the domain of grids (systems of linear congruences) led to the definition of a functionally complete set of abstract operators, allowing for its integration into existing static analysis frameworks. Another research topic considered was the general problem of deciding whether or not the union of two numerical abstractions can be represented, without precision losses, by a single element of the considered abstract domain: several new algorithms have been proposed for the more popular domains, included a new algorithm for convex polyhedra that significantly improves upon the efficiency of previous approaches.

Another part of the research work is devoted to the systematic design of widening operators, which are those operators used to enforce and/or accelerate the termination of the analysis. Besides defining and providing an experimental evaluation for several operators for specific abstract domains, the research work lead to the definition of two general frameworks: in the first one, the precision of an existing widening operator is improved by enriching its definition with a set of heuristics that, taken in isolation, would compromise the convergence guarantee; a second framework allows for the definition of widening operators working on finite, disjunctive collections of abstract elements, starting from an existing widening defined on the underlying abstract domain.

Most of the research activity carried out is characterized by an experimental evaluation phase that is meant to validate the theoretical results achieved. Such a systematic approach, pursued together with the coauthors, resulted in a strong collaboration to the development of several innovative software projects: the Parma Polyhedra Library (PPL), a library of numerical abstractions targeted at static analysis and verification of hardware and software systems; China, a static analyzer for constraint logic programs; ECLAIR, a precise and efficient static analyzer for mainstream imperative languages, such as C and C++. Most of the research activity has also been directly applied in the context of the university spin-off BUGSENG srl, where he collaborated to the development of static analysis tools since its foundation until 2014.

During his research activity, besides serving as a referee for international journals and conferences, Enea Zaffanella was a member of program committees for several national and international workshops and conferences: Joint Conference on Declarative Programming (APPIA-GULP-PRODE), Convegno Italiano di Logica Computazionale (CILC), Workshop on Logic-Based Methods in Programming Environments (WLPE), Workshop on Numerical and Symbolic Abstract Domains (NSAD), Static Analysis Symposium (SAS). He participated to several national and international research projects: ESPRIT Basic Research Action n. 6707 ("ParForce"); COFIN'99 "Automatic Program Certification by Abstract Interpretation" COFIN'00 "Abstract Interpretation, Type Systems and Control-Flow Analysis" COFIN'01 "Aggregate- and Number-Reasoning for Computing" PRIN'02 "Constraint Based Verification of Reactive Systems" PRIN'04 "AIDA - Abstract Interpretation Design and Applications" PRIN'07 "AIDA2007 - Abstract Interpretation Design and Applications" Italy-Spain bilateral project IT229 "Advanced Development Environment for Logic Programs".