Résumé
Les annotations de programme, sous forme de pré/postconditions de fonctions, sont cruciales pour accomplir différentes tâches, de l'ingénierie logicielle à la vérification de code. Malheureusement, ces annotations sont rarement fournies et doivent donc être rétro-ingéniées manuellement. Dans notre article, nous étudions comment l'acquisition de contraintes peut être utilisée pour inférer des préconditions. Cela a conduit à PRECA, un outil qui infère des préconditions à partir d'observations d'exécution du code uniquement, et assurant des garanties claires de correction. Mots-clés Acquisition de contraintes, analyse de code, préconditions