[ job | fulltime | Paris ] Développeur principal à plein temps d'Alt-Ergo chez OCamlPro

Alt-Ergo est l’un des solveurs SMT les plus efficaces pour la vérification formelle de code. Il est ainsi utilisé derrière des ateliers tels que Why3, Frama-C et Spark. Initialement développé par Sylvain Conchon au LRI, il est aujourd’hui maintenu par OCamlPro, grâce aux financements du Club Alt-Ergo (AdaCore, Trust-in-Soft, Thalès, MERCE, CEA List), à des contrats bilatéraux d’évolution et à des projets collaboratifs.

OCamlPro souhaite aujourd’hui recruter un développeur principal à temps plein pour Alt-Ergo, pour compléter son équipe méthodes formelles et accélérer l’évolution d’Alt-Ergo. Disposant d’une expérience dans les méthodes formelles, ses missions seront :

  • de découvrir le projet Alt-Ergo et tous ses composants (prouveur, interface graphique, etc.) et d’en comprendre le fonctionnement à travers l’exploration du code et la lecture d’articles scientifiques;

  • d’élaborer la roadmap de maintenance évolutive d’Alt-Ergo, en collaboration avec les membres du Club Alt-Ergo, et de proposer des améliorations qui pourront être financées au travers de contrats
    bilatéraux ou de projets collaboratifs;

  • de participer avec l’équipe à la maintenance corrective d’Alt-Ergo et de fournir du support aux membres du Club Alt-Ergo;

  • de participer à l’encadrement de stages et de thèses CIFRE autour d’Alt-Ergo et des solveurs SMT en général;

  • de suivre l’actualité des solveurs SMTs et des travaux scientifiques connexes, et de maintenir des collaborations avec les experts académiques du domaine;

Intégré au sein de l’équipe Méthodes Formelles d’OCamlPro, il bénéficiera de leur expérience et leur fera bénéficier de son expertise croissante dans l’utilisation d’Alt-Ergo. Outre la maintenance d’Alt-Ergo, l’équipe Méthodes Formelles d’OCamlPro participe à diverses activités:

  • Développement d’outils open-source pour les méthodes formelles, tels que Dolmen, Matla, etc.

  • Expertises sur WhyML, TLA, Coq, et autres langages de spécification et de vérification;

  • Certification de logiciels pour les Critères Communs (EAL6 et plus)

  • Spécification et vérification formelle de smart contracts (Solidity, etc.)

Les bureaux d’OCamlPro sont dans le 14ème arrondissement de Paris (Alésia). L’entreprise est connue pour son équipe sympathique, son excellence technique, sa productivité, ses valeurs et son éthique.

Si ce poste vous intéresse, n’hésitez pas à envoyer votre CV à:

contact@ocamlpro.com

Pour plus d’informations sur OCamlPro:

Pour plus d’informations sur Alt-Ergo:

https://alt-ergo.ocamlpro.com/

Pour plus d’informations sur le Club Alt-Ergo:

7 Likes