[TYPES/announce] PhD fellowship at LaBRI, Bordeaux France

[Sylvain Salvati]

Please distribute this announcement to the student who may be interested.

PhD Position at LaBRI Bordeaux France

Subject: higher-order verification.

The position will be fully funded for three years for obtaining a PhD in
computer science from the University of Bordeaux. It is to start in
autumn 2016.

The applicant is required to have a strong background in theoretical
computer science. More specifically, knowledge in the following fields
will improve the applicant chances:
- lambda-calculus
- finite state automata and logic
- abstract interpretation

The gross salary is of €1684.93 per month, which amounts to about
€1356.83 after tax. The position also comes with opportunities to
teach after the first year (at Bordeaux University or another academic
institution of Bordeaux), which yield extra salary (it then typically
reaches about €1,800 after tax).

The LaBRI is a vivid laboratory with about 300 researchers (including
PhD students and postdocs). It has a lively atmosphere with regular
seminars and an international dimension that stimulates the exchange
of ideas. Bordeaux is a lively academic city in the south-west of
France. It is a UNESCO World-Heritage site, has an active cultural
scene, and quite reasonable living costs.


To apply send us a CV (including the detail of attended courses and
grades) a motivation letter and references before September
9th by email:

- Sylvain Salvati <salvati at labri.fr>
- Igor Walukiewicz <igw at labri.fr>

--Details

Higher-order features are now largely adopted by mainstream languages
such as Java, Javascript, or Python. As software has become by and
large reactive, specifications are required to describe its behavior
in the environment. This calls for automated verification methods of
behavioural properties of higher-order programs.

We have shown that many behavioral properties can be reduced to
evaluating programs in finite domains. As these domains can be very
large, efficient methods are needed to compute the values of programs
in finite models. The goal of the PhD is to pursue and combine two
strategies for obtaining such methods. The first strategy consists in
extending techniques of abstract interpretation that have been
very successful for safety properties of first-order programs. The
second strategy is to take advantage of the structure of the
interpretation domains, in particular of aspects related to
linearity and to determinism.