Automated Program Analysis: Revisiting Precondition Inference through Constraint Acquisition
Authors: Grégoire Menguy, Sébastien Bardin, Nadjib Lazaar, Arnaud Gotlieb
IJCAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | 6 Experimental Evaluation We implemented PRECA1 in JAVA, and rely on the CHOCO constraint solver and MINISAT SAT solver. We evaluate PRECA on the following Research Questions: RQ1 Can PRECA handle realistic functions? ... We experimentally evaluate the benefits of our technique on several benchmark functions (Section 6.1). The results show that PRECA significantly outperforms prior precondition learners, be it black-boxes or white-boxes which came as a surprise. |
| Researcher Affiliation | Academia | Gr egoire Menguy1 , S ebastien Bardin1 , Nadjib Lazaar2 and Arnaud Gotlieb3 1Universit e Paris-Saclay, CEA, List, Palaiseau, France 2LIRMM, University of Montpellier, CNRS, Montpellier, France 3Simula Research Laboratory, Oslo, Norway |
| Pseudocode | Yes | Algorithm 1: PRECA |
| Open Source Code | Yes | We implemented PRECA1 in JAVA, and rely on the CHOCO constraint solver and MINISAT SAT solver. 1https://github.com/binsec/preca |
| Open Datasets | Yes | Our benchmark considers 50 real C functions. It contains all functions from string.h, all functions from [Seghir and Kroening, 2013; Sankaranarayanan et al., 2008] (except 2 functions from an old Xen version), functions from the DSA benchmark (https://tinyurl.com/tvzzpvmm), Frama C WP test suite (https://tinyurl.com/ycxdbjf3), Siemens suite [Hutchins et al., 1994] and the book Science of Programming [Gries, 2012]. |
| Dataset Splits | No | The paper discusses generating test cases for active learning but does not specify standard training/validation/test dataset splits with percentages, sample counts, or citations to predefined splits. |
| Hardware Specification | Yes | Experiments are done on a machine with 6 Intel Xeon E-2176M CPUs and 32 GB of RAM. |
| Software Dependencies | No | The paper mentions 'JAVA', 'CHOCO constraint solver' and 'MINISAT SAT solver' but does not provide specific version numbers for these software components. |
| Experiment Setup | Yes | We run PRECA with different time budgets per function (from 1s to 1h) and an oracle timeout of 1min (leading to the ukn answers). |