Un événement

GDR Sécurité Informatique Region Centre Val de Loire

organisé par 

Le Laboratoire d'Informatique Fondamentale d'Orleans INSA Val de Loire
Automated Program Analysis: Revisiting Precondition Inference through Constraint Acquisition
Grégoire Menguy  1@  
1 : Direction de Recherche Technologique (CEA)
Commissariat à l'énergie atomique et aux énergies alternatives, CEA-LIST

Program annotations under the form of function pre/postconditions are crucial for many software engineering and program verification applications. Unfortunately, such annotations are rarely available and must be retrofit by hand. In this paper, we explore how Constraint Acquisition (CA), a learning framework from Constraint Programming, can be leveraged to automatically infer program preconditions in a black-box manner, from input-output observations. We propose PreCA, the first ever framework based on active constraint acquisition dedicated to infer memory-related preconditions. PreCA overpasses prior techniques based on program analysis and formal methods, offering well-identified guarantees and returning more precise results in practice.


Personnes connectées : 3 Vie privée
Chargement...