[isabelle] [gdr.gpl ] PhD and Postdoc positions at IRISA/Inria Rennes

CELTIQUE is looking for PhD candidates and postdocs!

The IRISA/Inria Celtique group in Rennes (France) has several open PhD and
post-doctoral position. The positions are funded by David Pichardie's european ERC VESTA project (2018-2023). Postdoc applicants must have a PhD in Computer
Science. PhD applicants must have a Master in Computer Science. We seek
candidates with a solid theoretical background in Computer Science, in at least
one of the following topics: - formal semantics of programming languages
- compiler implementation
- abstract interpretation
- Coq proof assistant

Postdoc positions are one year, with the possibility of extension to a second
year. All position may start after September 1st 2018.

Candidate that are specially interested by compiler verification will also be
considered for a postdoc in the national ANR project Discover
(http://discover.irisa.fr/), and can negotiate a starting time earlier than

The working language is English, knowledge of French is not required. The successful candidate will join the Celtique team at IRISA, INRIA Rennes:

Applicants should send their curriculum vitae, cover letter and names/contact
information of two references to David Pichardie
(david.pichardie at ens-rennes.fr). Recommandation letters should be sentto David
Pichardie directly.

Potential research projects
- Verification of static analysis with the Coq proof assistant
- Formal verification of abstract interpreters using the Galois connection
  framework inside Coq
- Formal verification of state-of-the-art SSA-based compiler optimisations
- Advanced abstract interpretation for software security (Java, C, or assembly
- Innovative techniques for extraction of efficient code with Coq

Plus d'infos sur le GDR GPL : http://gdr-gpl.cnrs.fr

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.