Contract type : Public service fixed-term contract
Level of qualifications required : PhD or equivalent
Fonction : Post-Doctoral Research Visit
About the research centre or Inria department
Inria, the French national research institute for the digital sciences, promotes scientific excellence and technology transfer to maximise its impact.
It employs 2,400 people. Its 200 agile project teams, generally with academic partners, involve more than 3,000 scientists in meeting the challenges of computer science and mathematics, often at the interface of other disciplines.
Inria works with many companies and has assisted in the creation of over 160 startups.
It strives to meet the challenges of the digital transformation of science, society and the economy.
The Celtique team develops mechanised semantics for full-fledged
programming languages focusing on the source C language and
efforts related to the implementation of source languages. This
includes the formal study of intermediate representations used in
optimizing compilation chains, or runtime environment components.
A particular effort is dedicated to the semantic modeling and analysis
of intermediate representations such as those found in modern
optimizing compilers, e.g. SSA and variants thereof. We build on the
CompCert C compiler , which is mainly developed by X. Leroy from
the EPI Gallium. CompCert is an industrial-strength C compiler which
is both programmed and proved correct inside the Coq proof
assistant. This is a flagship of formal verification which is the
cornerstone of national (ANR Verasco) and international research
projects (NSF DeepSpec).
The actual CompCert C compiler does not use SSA-based optimization
techniques. In the Celtique team, we study this particular techniques
through the CompCertSSA middle-end , that we started to develop in the
team several years ago now. CompcertSSA extends Compcert with a
optimizing middle-end based on the SSA (Static Single Assignment)
form. Currently, the compiler has satisfying performance in terms of
compile-time and running-time of generated code, but there are a
couple of remaining open problems we would like to explore.
In particular, we would like to improve it with techniques relying on
the explicit representation of data and control-dependencies of
programs. It improves on the initial SSA form, which was initially
seen as a simple control-flow-graph. Examples of such techniques
include the Program Dependence Graph, Sea-of-Nodes , of Monadic
Gated SSA 
The challenge here is to shift from an operational setting where an
abstract machine is running instructions one after another, to a more
equational view of program behaviours, where data and control
dependencies are what drive the program execution. Additonnally, we
will need to design adequate reasoning and proof techniques that scale
to large mechanized developments such as realistic verified compilers.
We have started to work in this direction on SSA variants such as the
Sea-of-Nodes , and we would like to start working on the monadic
gated SSA form .
A short-to-middle term objective is the formal definition of an
equational semantics for SSA, perhaps reusing ideas from the
synchronous languages community where programs are seen as value
streams generators. In the context of verified compilation, one of the
main challenges is to be able to relate such an equational semantics
back to its operational version, which is essentially what is actually
implemented by the compiler backend. The long-term goal is to make
this semantic approach a foundation of verified program optimizers, or
verified translation validators, embedded in optimizing verified
 Xavier Leroy. Formal verification of a realistic
compiler. Communications of the ACM, 52(7):107--115, 2009.
 Gilles Barthe, Delphine Demange, David Pichardie. Formal
Verification of an SSA-based Middle-end for CompCert. ACM Transactions
on Programming Languages and Systems (TOPLAS), ACM, 2014, 36 (1), pp.35.
 Cliff Click. 1995. Global code motion/global value numbering. In
Proceedings of the ACM SIGPLAN 1995 conference on Programming language
design and implementation (PLDI '95). ACM, New York, NY, USA, 246-257.
 Jean-Baptiste Tristan, Paul Govereau, and Greg
Morrisett. 2011. Evaluating value-graph translation validation for
LLVM. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming
Language Design and Implementation (PLDI '11). ACM, New York, NY, USA, 295-305.
 Delphine Demange, Yon Fernández de Retana, David
Pichardie. Semantic reasoning about the sea of nodes. CC 2018 – 27th
International Conference on Compiler Construction, Feb 2018, Vienna, Austria. ACM Press, pp.163-173.
- Design and implement efficient validation techniques for SSA-based optimizations
- Semantic characterization of the validation process, proof of correctness
- Contribute to the state-of-the-art of compilers formal verification
- Disseminate new contributions in international conferences or journals
- PhD in Computer Science
- Background in optimizing compilers techniques
- Background in SSA-based optimization techniques
- Background in formal verification in interactive proof assistants
- Fluent in English
- Ability to work in team
- Subsidized meals
- Partial reimbursement of public transport costs
Monthly gross salary amounting to 2 653 euros
- Theme/Domain :
Proofs and Verification
Software engineering (BAP E)
- Town/city : Rennes
- Inria Center : CRI Rennes - Bretagne Atlantique
- Starting date : 2019-09-01
- Duration of contract : 1 year, 4 months
- Deadline to apply : 2019-04-30
The keys to success
Applicants must have a PhD in Computer Science. We seek candidates
with a strong background in Computer Science with an interest in at
least one of the following topics: formal semantics, programming
languages, compiler implementation, interactive theorem
provers. Applicants should have a strong theoretical background, but
also some experience with software development.
The position is for 18 months minimum and the starting date is
flexible to some extent. The working language is English, knowledge
of French is not required. The successful candidate will join the
Celtique team at Inria Rennes: https://team.inria.fr/celtique/
Inria, the French national research institute for the digital sciences, promotes scientific excellence and technology transfer to maximise its impact. It employs 2,400 people. Its 200 agile project teams, generally with academic partners, involve more than 3,000 scientists in meeting the challenges of computer science and mathematics, often at the interface of other disciplines. Inria works with many companies and has assisted in the creation of over 160 startups. It strives to meet the challenges of the digital transformation of science, society and the economy.
Instruction to apply
Please submit online : your resume, cover letter and letters of recommendation eventually
Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.
Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.
Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.