This is an announcement for a postdoctoral position in the CAVOC project (Compositional Automated Verification for OCaml Code). The post-doc will take place in Nantes, France. It will be co-supervised by Guilhem Jaber (Nantes Université and Inria Gallinette team) and Gabriel Radanne (Inria CASH team).
It aims to bring together approaches from abstract interpretation, model checking, and game semantics to statically analyze OCaml code.
The successful candidate will be employed by Inria and work in the Gallinette team (https://gallinette.inria.fr), at Nantes University. The position is for one year, and should start in the first semester of 2024 (to be negociated). The salary will depend on the successful candidate’s prior research experience with a guaranteed minimum of ~2200€/month after taxes. The working language can either be English or French.
We seek candidates holding a PhD in Computer Science or Mathematics, and with expertise in programming language semantics, λ-calculi, type theory, functional programming, abstract interpretation, compilation, model checking, or program logic.
Profile
The candidate should be familiar with formal approaches in programming language design, notably type systems, semantics, and logic. More concretely, knowledge of the OCaml programming language is expected, and a knowledge of abstract interpretation or model checking would be highly appreciated.
This postdoc strongly relies on the fact that practical implementation should have strong theoretical foundations and that further refinements of the theory should get inspiration from the practical side.
Application process
- Applications will be processed starting the 18th of December. Late applications will be considered until the position is filled.
- You do not need to have defended your PhD thesis to apply, but you will need to have obtained your PhD to start the contract.
- Candidates can send their application to Guilhem Jaber (guilhem dot jaber at inria dot fr) and Gabriel Radanne (gabriel dot radanne at inria do fr) with a subject containing “[CAVOC post-doc application]“.
- The application should contain a CV, two selected publications and two contacts of reference persons (or reference letters if available).
Context
The CAVOC project aims to develop a sound and precise static analyzer for OCaml, that can catch large classes of bugs represented by uncaught exceptions.
The analyzer reasons compositionally on programs, in order to analyze them at the granularity of a function or of a module. It takes into account the abstraction properties provided
by the type system and the module system of the language: local values, abstracted definitions of types, parametric polymorphism.
The main goal is to be sound in a strong way: if an OCaml module is considered to be correct by the analyzer, then one will have the guarantee that no OCaml code interacting with this module can trigger uncaught exceptions coming from the code of this module.
To model the behaviour of a module, we rely on game semantics, where programs formed by a module and a client of the module are modeled as calls-and-returns interactions. A module is then represented as a transition system that generates traces representing the interaction with any possible client. This transition system is directly generated from the module’s code
(implementation and signature), using an operational semantics. We have implemented such an interactive semantics for a large fragment of OCaml, which we are using to develop our prototype analyzer.