- Invariant Synthesis for Programs Manipulating Lists with Unbounded Data
A. Bouajjani, C. Dragoi, C. Enea, A. Rezine, and M. Sighireanu
CAV'10.
Introduction of heap abstract domains with data constraints for intra-procedural analysis, the basis of CINV.[pdf, pdf long version]
- On Inter-Procedural Analysis of Programs with Lists and Data
A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu
PLDI'11.
Extension of CINV to inter-procedural analysis, the basis of Celia.
- Automated verification of heap-manipulating programs with infinite data .
C. Dragoi
PhD Thesis, December 2011.
Detailed presentation of the abstract domains and of the analysis method.
- Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data
A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu
VMCAI'12.
Overview of the analysis and verification methods.
- Accurate Invariant Checking for List-Manipulating Programs with Infinite Data
A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu
submitted.
Verification of C programs.