Name: Pierre Ganty 
Place: IMDEA Software (public research institute), Madrid, Spain.
Duration: between 4 and 6 months

The goal of the internship is to realize a prototype tool that finds bugs in
multithreaded procedural programs where the threads communicate through a
shared global memory.

The question that asks if such a program contains a bug (like an execution to a
set of bad program configurations) is unsolvable with a computer program, even
if one assume all the data variables range over a finite domain.  However the
problem can be given a partial answer using, for instance.
underapproximations. An underapproximated analysis is useful to discover bugs
but is pointless to prove their absence.

A practical underapproximated analysis is the context bounded switches
approach (applied, for instance, at Microsoft). The context bounded switches
approach is successful as long as the bound on the number of context switches
(a context switch is a reallocation of the CPU from one thread to another)
remains small.  Unfortunately, for some programs, bugs are not exposed by small
number of context switches.  Recently, we have generalized the bounded context
switch approach. The underapproximated analysis we defined is able to consider
an arbitrary number of context switches. 

In our approach, the sequence of context switches that are examined are not
limited in length (as does the context bounded switches approach) but they have
to match a certain pattern given by a so called bounded language. A bounded
language is a language of the form w1* ...  wn* where w1,..., wn are finite
sequences of context switches. It is clear from the use of the Kleene star that
some sequences of unbounded length are now examined, contrary to the context
bounded switches approach.  

The purpose of the internship is to investigate if this theoretical advantage
transposes in practice. The intern will define analysis techniques and
implement a tool based on bounded languages. This will require to review the
literature on the subject, solve challenging scientific problems to define
efficient algorithms, and implement them inside a prototype tool. Finally the
prototype would go under an empirical comparison against the tools based on
context bounded switches approach.