[TYPES/announce] PhD Positions at Inria Grenoble, France

[Pierre Geneves]

The Tyrex research team at Inria Grenoble (http://tyrex.inria.fr)
has open positions for PhD students:

         http://tyrex.inria.fr/jobs.html

In particular, we have an open position on the following topic:

Soundy Analysis Techniques for Web Development

XQuery [1] is the standard language language dedicated to XML data
querying and manipulation. As opposed to other NoSQL languages (and
e.g. XSLT in particular), it has been intended to feature strong
static typing [5].

As emphasized in [4], “static program analysis is a key component of
many software development tools, including compilers, development
environments, and verification tools. Analyses are often expected to
be sound in that their result models all possible executions of the
program under analysis. Soundness implies that the analysis computes
an over-approximation in order to stay tractable [5]; the analysis
result will also model behaviors that do not actually occur in any
program execution. The precision of an analysis is the degree to which
it avoids such spurious results. Users expect analyses to be sound as
a matter of course, and desire analyses to be as precise as possible,
while being able to scale to large programs.”

It was shown in [2] that sound yet precise static analyses are
possible for an XQuery fragment [2], even for complex expressions that
navigate in XML trees [2,3]. While soundness seems essential for any
kind of static program analysis, approximations and omissions are
usually required for language features when applied to real programs.
This is coined by the recent concept of soundiness [4] which defines
“soundy analyses”: a soundy analysis aims to be as sound as possible
without excessively compromising precision or scalability.

The goal of this internship is to investigate methods of code analysis
which take advantage of sound verification systems developed for
XQuery language fragments in the literature (such as [2]) to
efficiently compute useful guarantees on real XQuery code used in
production.

Specifically, the subject will consist of:

  – identifying different levels of static analyses corresponding to
    relevant language fragments;
  – supplementing sound analysis techniques with relevant
    approximations to make the most of them with real-world code;
  – investigating the concept of soundiness [4] in the context of
    XQuery;
  – implementing a prototype checker which is capable of running on
    real production code while indicating meaningful guarantees that
    can be provided.

Real-world XQuery code will be provided by a startup in the domain of
XQuery-based web development frameworks.

  
References:

      [1] XQuery 3.0: An XML Query Language, W3C Recommendation 08
      April 2014:https://www.w3.org/TR/xquery-30/

      [2] XQuery and Static Typing: Tackling the Problem of Backward
      Axes. Pierre Geneves and Nils Gesbert. In International
      Conference on Functional Programming (ICFP) 2015
      (https://hal.inria.fr/hal-01082635v2/document)

      [3] Efficient Static Analysis of XML Paths and Types. Pierre
      Genevès, Nabil Layaïda, Alan Schmitt. In ACM SIGPLAN conference
      on Programming language design and implementation (PLDI) 2007
      (https://hal.inria.fr/inria-00502789/document)

      [4] In Defense of Soundiness: A Manifesto. Ben Livshits, Manu
      Sridharan, Yannis Smaragdakis, Ondřej Lhoták, J. Nelson Amaral,
      Bor-Yuh, Evan Chang, Sam Guyer, Uday Khedker, Anders Møller and
      Dimitrios Vardoulakis. In Communications of the ACM, 2015.
      http://soundiness.org/

      [5] Course: Introduction to XQuery and Static Type-Checking.
      University Grenoble Alpes. Pierre Genevès.
      http://tyrex.inria.fr/courses/mosig2015/xquery.pdf


Environment:
     The doctoral work is to be carried out in the Tyrex research team
     (http://tyrex.inria.fr). Tyrex has a long research experience in
     the area of the web and particularly in the static analysis of web
     query languages through logical modeling and reasoning. The team
     has a tradition of conducting research both at the theoretical and
     applied (implementation) levels. Tyrex members regularly
     participate in the most relevant conferences of the domain
     (including major venues concerning the web, programming languages,
     and artificial intelligence). As such, it is an excellent and
     stimulating environment for ambitious PhD candidates. The PhD
     candidate will also benefit from the national and international
     collaborations of the team. The position is located at Inria
     Grenoble Rhône-Alpes (http://www.inria.fr/centre/grenoble),
     Montbonnot (near Grenoble, France) which is a major research
     laboratory in Computer Science offering a stimulating research
     environment.

Contact:
     Pierre Genevès (HDR) (pierre.geneves at cnrs.fr),
     Nils Gesbert (nils.gesbert at grenoble-inp.fr),
     Nabil Layaïda (HDR) (nabil.layaida at inria.fr)


Keywords:
     Static typing, structured data, data-centric programming


-- 
Pierre Genevès, Ph.D., HDR
Responsable permanent, équipe Tyrex
LIG - Inria - UGA - CNRS - Grenoble INP
Responsable de spécialité Informatique, ED MSTII
pierre.geneves at cnrs.fr
(33)476615281
http://tyrex.inria.fr

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20170303/fcfe5835/attachment-0001.html>