Logic List Mailing Archive

PhD position on higher-order verification, Bordeaux (France), Deadline: 9 Sep 2016

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 EUR 1684.93 per month, which amounts to about EUR 
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 EUR 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@labri.fr>
- Igor Walukiewicz <igw@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.
--
[LOGIC] mailing list
http://www.dvmlg.de/mailingliste.html
Archive: http://www.illc.uva.nl/LogicList/

provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam