@article{18074,
  author = {Gr{\'e}goire Menguy and Sebastien Bardin and Arnaud Gotlieb and Nadjib Lazaar},
  title = {A Query-Based Constraint Acquisition Approach for Enhanced Precision in Program Precondition Inference},
  abstract = {Program annotations in the form of function pre/postconditions play a crucial role in various software engineering and program verification tasks. However, the frequent absence of these annotations necessitates manual retrofitting. This paper shows how constraint acquisition, a learning framework derived from constraint programming and version space learning, can be extended for the autonomous inference of program preconditions in a black-box manner. Through automatically generated queries, this inference relies solely on input-output observations of program executions. We introduce PreCA, the first-ever precondition inference framework leveraging query-based constraint acquisition. Notably, we specialize PreCA to handle memory-related preconditions on binary code, which pose significant challenges in the context of data and information management systems. In contrast to prior black-box techniques, PreCA provides well-defined guarantees. Specifically, it employs a sound and complete method to generate preconditions consistent with all the observed input-output relationships of the program. Furthermore, empirical evaluations on our benchmark demonstrate that PreCA outperforms the results of state-of-the-art approaches, delivering comparable or superior results in 5s, as opposed to the 1-hour runtime of existing approaches on identical machines. Notably, we present two use cases from the standard libc and the mbedtls cryptographic library where PreCA infers more precise preconditions than those derived from the documentation},
  year = {2025},
  journal = {Journal of Artificial Intelligence Research},
  publisher = {AI Access Foundation},
  url = {https://www.jair.org/index.php/jair},
}