En poursuivant votre navigation sur ce site, vous acceptez le dépôt de cookies dans votre navigateur. (En savoir plus)

H/F contrat doctoral SAT pour la vérification formelle en méthode B

Cette offre est disponible dans les langues suivantes :
Français - Anglais

Date Limite Candidature : mercredi 7 décembre 2022

Assurez-vous que votre profil candidat soit correctement renseigné avant de postuler. Les informations de votre profil complètent celles associées à chaque candidature. Afin d’augmenter votre visibilité sur notre Portail Emploi et ainsi permettre aux recruteurs de consulter votre profil candidat, vous avez la possibilité de déposer votre CV dans notre CVThèque en un clic !

Informations générales

Référence : UMR8188-DANLEB-003
Lieu de travail : LENS
Date de publication : mercredi 26 octobre 2022
Nom du responsable scientifique : Daniel Le Berre
Type de contrat : CDD Doctorant/Contrat doctoral
Durée du contrat : 36 mois
Date de début de la thèse : 1 janvier 2023
Quotité de travail : Temps complet
Rémunération : 2 135,00 € brut mensuel

Description du sujet de thèse

Le projet ANR BLaSST vise à établir un pont entre les techniques combinatoires et symboliques dans la preuve automatique de théorèmes, en particulier pour les obligations de preuve générées à partir de modèles B. Des travaux seront menés sur des techniques basées sur SAT ainsi que sur des formalismes SMT plus expressifs. Dans les deux cas, les techniques d'encodage, les techniques de résolution optimisée, la génération de modèles et la suggestion de lemmes seront considérées. En combinant les deux lignes de travail, l'impact scientifique attendu est un degré substantiellement plus élevé d'automatisation des solveurs pour des langages d'entrée expressifs en exploitant le raisonnement d'ordre supérieur et les instanciations énumératives sur des domaines finis. L'efficacité des techniques développées dans le projet sera quantifiée en les appliquant à des ensembles de référence fournis par le partenaire industriel. L'impact industriel de BLaSST sera une plus grande productivité des ingénieurs de preuve.

BLaSST réunit des experts académiques en techniques de raisonnement automatisé (CRIL, INRIA et Université de Liège) et une société industrielle (CLEARSY) leader en méthodes formelles pour un effort de 4 ans qui vise à fournir une percée dans la vérification formelle appliquée à la conception de logiciels.

L'objectif principal de cette thèse est de tirer parti des technologies SAT pour aborder différentes tâches de raisonnement pour les développements formels de logiciels, en particulier dans des approches telles que la méthode B. En effet, cette thèse se concentrera sur le développement et l'optimisation des encodages et des techniques basés sur SAT afin d'atteindre les objectifs suivants :

Développer différents encodages basés sur SAT pour générer des contre-exemples d'obligations de preuve.

Développer une méthode pour construire des suggestions de preuve en relation avec les codages SAT proposés pour aider à montrer les obligations de preuve.

Développer une méthode d'identification des prémisses manquantes pour établir la validité.

La recherche sera menée en étroite collaboration avec notre partenaire industriel CLEARSY.

Profil du candidat

Nous recherchons un candidat au doctorat ayant un master (ou équivalent) en informatique avec une expérience en logique. Une connaissance préalable du raisonnement automatique ou des méthodes formelles (TLA+, B, Z ou Alloy par exemple) est un plus. Le candidat doit maîtriser un langage de programmation courant tel que C, C++ ou Java.

Plus de détails sur ce sujet de thèse sont disponibles sur le site du laboratoire d'accueil : https://www.cril.univ-artois.fr/phds/phdblasst/

Contexte de travail

La thèse se déroulera au sein du CRIL (http://www.cril.fr/), dans le cadre du projet ANR PRCE BLaSST, dont les autres partenaires sont INRIA Nancy, l'université de Liège et la société CLEARSY.

On en parle sur Twitter !