Combiner machine learning symbolique et méthodes formelles pour l'inférence automatique de spécification de code

Les contrats de fonctions, sous la forme de pré- / post-conditions, permettent de specifier le comportement de fonctions. Ces contrats sont donc cruciaux pour améliorer la sécurité des programmes et réaliser différentes tâches, de l'ingénierie logicielle à la vérification de code. Malheureusement, ceux-ci sont rarement fournis et doivent donc être rétro-ingéniés à la main. Le but de ce travail est de comprendre comment combiner le machine learning symbolique et les méthodes formelles pour inférer de manière automatique les contrats de fonctions complexes. L'objectif est de tirer profit des points forts de chacun pour créer des méthodes capables d'inférer ces contrats de manière efficace et avec des garanties claires de correction. Ces méthodes devront fonctionner sur des programmes difficiles à analyser par les approches statiques usuelles comme les codes hautement optimisés ou obfusqués. Nous nous concentrerons en particulier sur la combinaison des méthodes d'acquisition de contraintes et de l'exécution symbolique.