Analyse de Code Automatique: Revisiter l'Inférence de Préconditions via l'Acquisition de Contraintes - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier
Conference Papers Year : 2023

Analyse de Code Automatique: Revisiter l'Inférence de Préconditions via l'Acquisition de Contraintes

Abstract

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
Fichier principal
Vignette du fichier
Actes_CH_PFIA2023_3_ pages81-82.pdf (460.2 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

lirmm-04473797 , version 1 (22-02-2024)

Identifiers

  • HAL Id : lirmm-04473797 , version 1

Cite

Grégoire Menguy, Sébastien Bardin, Nadjib Lazaar, Arnaud Gotlieb. Analyse de Code Automatique: Revisiter l'Inférence de Préconditions via l'Acquisition de Contraintes. JFPC 2023 - Journées Francophones de Programmation par Contraintes@PFIA2023, Jul 2023, Strasbourg, France. pp.81-82. ⟨lirmm-04473797⟩
95 View
29 Download

Share

More