| Supervisor | Antoine Miné |
|---|---|
| Internship location | Abstraction team Département d'informatique École normale supérieure 45, rue d'Ulm Paris, France |
| Relevant course | M2-6: Abstract interpretation: application to verification and static analysis |
The verification problem for parallel software is far more complex than for sequential ones, due to the huge number of interleavings of thread executions one has to consider. Thread-modular methods, such as rely/guarantee, side-step this issue by decomposing the verification of the whole program into the independent verification of each thread in an environment modeling the action of the other threads. In the context of static analysis, a thread-modular analysis infers intra-thread local invariants and inter-thread interferences, both of which are (complementary) abstract interpretations of the program trace semantics. Most static analyses abstract interferences very coarsely, as (an abstraction of) the set of values each thread can store into each variable during its whole execution, which is very efficient but imprecise.
The goal of the internship is to develop new abstractions of interferences which are more expressive and more precise than existing ones, without sacrificing scalability. Promising directions include the design of abstractions that are (at least partially) flow-sensitive or relational.
The intern will develop new abstractions for interferences, including all the operators and transfer functions required by a static analyzer. Each proposed domain and operator shall be proved correct, and motivated by its usefulness analyzing actual program fragments and by its tractable complexity. While not required, implementing and evaluating the domains experimentally is a plus.
The internship will take place in the context of the AstréeA Project which can provide realistic fragments of industrial parallel programs.
Note: other internships are possible on the topic of static analysis of parallel programs, and abstract interpretation in general. Please contact the internship supervisor for more information.