The Coq mailing list

[Frédéric Dabrowski <frederic.dabrowski AT univ-orleans.fr>]

L’université d’Orléans recrute un maître de conférence en section 27. Le profil est en particulier ouvert à des candidats dans le domaine de la sémantique des langages de programmation dont

l’intégration se fera dans l’équipe LMV (Langages, Modèles et vérification). L’équipe LMV travaille sur la sémantique des langages de programmation parallèle et concurrente et sur la vérification

de ce type de programmes.

La personne recherchée devra plus particulièrement s’intégrer dans au moins l’un des thèmes suivants :

• -  Modèles des langages de programmation

• -  Propriétés de correction sémantique des langages de programmation

• -  Correction de programme par analyse statique, test et preuve déductive (dataflow, interprétation abstraite, logique de séparation,...)

 - Certification d’outils d’analyse statique et de preuve déductive de programmes par assistants de preuve

Contact : F. Dabrowski, responsable de l’équipe LMV frederic.dabrowski AT univ-orleans.fr

Mots-clés :
Langages de programmation, sémantique formelle des langages de programmation, preuve de programmes, analyse de programmes, programmation réactive, programmation parallèle et concurrente. 

Nature du Poste: Maître de conférences
N° section : 27
Numéro du poste : 0482
Référence Galaxie : complétée ultérieurement par le SPE-EC
Profil succinct : Le poste proposé est un poste de maître de conférences à l’UFR Sciences et Techniques de l’Université d’Orléans, avec une intégration recherche au Laboratoire d’Informatique Fondamental d’Orléans (LIFO, EA 4022). L’enseignement concerne toutes les filières en informatique de l’UFR (Licence et Master en Informatique, et MIAGE). Au niveau recherche, la personne recrutée doit intégrer au choix une des deux équipes suivantes du LIFO : Langages, Modèles et Vérification (LMV) et Parallélisme, Distribution et Gestion de Données (Pamda).