My research interests concern with static analysis of programs via abstract interpretation.

Abstract interpretation
The key idea of static analysis is to verify some properties of a program for all its inputs. Because most of these problems are undecidable (e.g. they can not be solved by a computer) a way in order to approximate the behaviours of a program in a finite time is needed.
The abstract interpretation defines this approximation in mathematical terms. It has been discovered by Patrick and Radhia Cousot in 1977. The abstract interpretation framework requires to define a concrete semantics that specifies the properties on which the analysis is focused. Starting from it, an abstract semantics must be defined, related to the concrete one in a well-defined way. Finally a fixpoint function is required; in order to make convergent this function in a finite time, this function uses some operators (the least upper bound and, sometimes, the widening operators).
For more details about abstract interpretation (this paragraph contains just an intuition of that!) read this.

Multithreaded programs
In the last years an hot topic of the researchers' works has been the multithreaded programs, and in particular how to infer some properties on them at compile time.
The key idea of multithreaded programs is to let executed more than one thread parallely; different threads may communicate implicitily through a shared memory and they may synchronised through monitors, semaphores, etc... All the common programming languages support multithreading. Moreover multithread appears to be the most promising way in order to take fully advantage by single applications from multicore architecture.
Reasoning about multithread programs is strictly more complex than doing it on sequential programs. In particular, the parallel executions of different thread and their implicit communication on the shared memory may lead to non-deterministic behaviours really difficult to reproduce and to understand.

Java bytecode and CIL/MSIL
Both Java and the languages of the .Net framework as C# are compiled into an intermediate language that is in the middle between the source code and the assembler level. In particular this code is not structured but it is still readable.
Working at bytecode level has several advantages, and in particular you are in position to read and analyse the code of libraries. Moreover the instructions are quite simple. On the other hand, often it is not so easy to build the control flow graph of the programs, and many variables are introduced (and this may lead to a slower analysis).

Unsafe code
In C# the developers may defined some part of code as unsafe. In these areas, they can manipulate pointers as they did in the C programming language.
Working with pointers is a required feature in particular when you need to interface to operating system libraries written in C, to work with memory mapped devices, to develop performance-critical program, etc... The main problem of unsafe code is that through pointers you may read and write on parts of memory that have been previously allocated and so that belong to other procedures or programs. This type of bugs is really difficult to discover and reproduce by testing.
In this context a static analysis able to check at compile time if a pointer accedes or not to a non-allocated area of memory appears to be particularly interesting.