The Coq mailing list

[David Pichardie <david.pichardie AT inria.fr>]

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
September.

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

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
  programs)
- Innovative techniques for extraction of efficient code with Coq