[FM-India] [folli] PhD fellowship at LaBRI, Bordeaux, France

[Madhavan Mukund]

 ---------------------------- Original Message ----------------------------
 Subject: [folli] PhD fellowship at LaBRI, Bordeaux, France
 From:    "Sylvain Salvati" <sylvain.salvati at labri.fr>
 Date:    Fri, March 25, 2016 2:00 pm
 To:      folli at folli.info
 --------------------------------------------------------------------------
 
 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 Euro 1684.93 per month, which amounts to about
 Euro 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 Euro 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.
 
 ---------------------------------------------------------------------
 To unsubscribe, e-mail: folli-unsubscribe at folli.info
 For additional commands, e-mail: folli-help at folli.info