Les activités du laboratoire s’articuleront autour du développement d’outils de preuves formelles et de leur déploiement auprès des industriels pour la vérification des systèmes critiques.
C’est à l’occasion d’une journée technique organisée le 2 février dernier à Paris que l’éditeur franco-américain AdaCore, spécialisé dans les solutions logicielles pour le langage Ada, et l’Institut national de recherche en informatique et en automatique (Inria), au travers de son équipe de recherche Toccata spécialisée dans les spécifications formelles et les preuves assistées par ordinateur, ont annoncé le lancement opérationnel du laboratoire commun ProofInUse. Cogéré par AdaCore et l’Inria qui collaborent déjà ensemble depuis 2010, notamment sur le projet Hi-Lite, ProofInUse a vu sa création être validée au début de l’année dernière par l’Agence nationale de la recherche (ANR).
Les activités du laboratoire s’articuleront autour du développement d’outils de preuves formelles et de leur déploiement auprès des industriels pour la vérification des systèmes critiques. « Les deux grands axes de recherche sont l’amélioration des prouvers automatiques et une prise en compte de l’ensemble du langage Ada », indique Claude Marché, responsable de l’équipe Toccata et directeur du laboratoire ProofinUse. Grâce au financement sur trois ans de l’ANR (Agence nationale de la Recherche), deux ingénieurs ont rejoint le laboratoire commun, en plus des personnes d’AdaCore et de l’Inria qui travaillent déjà ensemble.
