Automated Program Analysis: Revisiting Precondition Inference through Constraint Acquisition

Automated Program Analysis: Revisiting Precondition Inference through Constraint Acquisition

Grégoire Menguy, Sébastien Bardin, Nadjib Lazaar, Arnaud Gotlieb

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence
Main Track. Pages 1873-1879. https://doi.org/10.24963/ijcai.2022/260

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.
Keywords:
Constraint Satisfaction and Optimization: Constraints and Machine Learning
Machine Learning: Active Learning
Multidisciplinary Topics and Applications: Software Engineering
Multidisciplinary Topics and Applications: Validation and Verification