Analyse de Code Automatique: Revisiter l'Inférence de Préconditions via l'Acquisition de Contraintes
Résumé
Program annotations under the form of function pre/postconditions are crucial for many software engineering and program verification applications. Unfortunately, these are rarely available and must be retrofit by hand. This paper explores how Constraint Acquisition (CA) can be leveraged to automatically infer program preconditions. This leads to P RE C A, which infers preconditions from input-output observations only, and presents clear correctness guarantees.
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
Origine : Fichiers produits par l'(les) auteur(s)