Développement de plug-in de preuve automatique dans l’Atelier B

CLEARSY est une PME Française fondée en 2001 par les ingénieurs auteurs de l’industrialisation de l’outil de modélisation formelle appelé Atelier B, utilisé pour spécifier, concevoir, valider les systèmes et réaliser les logiciels critiques (comme le pilote automatique du métro de la ligne 14 à Paris).

Rassemblant 150 ingénieurs répartis sur 4 pôles (Aix – Paris – Lyon – Strasbourg) CLEARSY participe aux projets stratégiques des grands industriels et donneurs d’ordres nationaux et internationaux.

Atelier B est un environnement de développement de composants logiciels et de spécification de systèmes mettant en œuvre les méthodes formelles B et Event-B (basées sur les mathématiques).

L’Atelier B est notamment utilisé par de grands constructeurs pour réaliser les logiciels de pilotage automatique de trains autonomes.

Lors de l’application de ces méthodes, sont produites des théorèmes que l’utilisateur doit vérifier. Pour cela, Atelier B dispose d’un démonstrateur automatique de théorèmes ainsi que d’une interface interactive de démonstration de théorèmes.

Il est prévu que les prochaines évolutions d’Atelier B permettent à l’utilisateur d’utiliser des outils tiers pour réaliser la vérification de théorèmes. L’intégration de ces outils se fera dans le cadre d’une infrastructure générique au moyen de « plug-ins » (pilotes) dédiés, composés : d’un outil de preuve automatique, d’un traducteur des obligations de preuve du format de Atelier B vers un format reconnu par l’outil, et d’un adaptateur interprétant les sorties de l’outil pour mettre à jour le statut de la preuve dans Atelier B.

On envisage de développer des traducteurs vers différents formats (SMT-LIB, TPTP, Why3, ZF, par exemple) ce qui permettra l’utilisation d’un grand nombre d’outils (Alt-Ergo, cvc4, SPASS, Yices2, Zenon, Zipperposition, Z3, pour en citer quelques-uns).

Location
  • Aix-en-Provence
Duration 6
Level 5

Postuler à cette offre de stage d'ingénieur

Pour postuler merci d’envoyer
un CV et une lettre de motivation
à l’adresse :

stages-ingenieurs@clearsy.com