about this paper

presentation abstract bibitem

downloads

paper (on HAL)
Jérôme Boillot and Jérôme Feret.
Abstraction of memory block manipulations by symbolic loop folding.
In Proceedings of the Thirty-fourth European Symposium on Programming, ESOP'25. Hamilton, Canada, V. Vafeiadis (Ed), To appear in Lecture Notes in Computer Science.
© Springer, Berlin, Germany.

Abstract: We introduce a new abstract domain for analyzing memory block manipulations, focusing on programs with dynamically allocated arrays. This domain computes properties universally quantified over the value of the loop counters, both for assignments and tests. These properties consist of equalities and comparison predicates involving abstract expressions, represented as affine forms in the loop counters and symbolic dereferences. All these methods have been incorporated within the Astrée static analyzer that checks for the absence of run-time errors in embedded critical software. We also give insights on how to implement this abstract domain within any other C static analyzer. 

@inproceedings{DBLP:conf/esop/BoillotF25,
  author       = {J{\'{e}}r{\^{o}}me Boillot and J{\'{e}}r{\^{o}}me Feret},
  editor       = {Viktor Vafeiadis},
  title        = {Abstraction of memory block manipulations by symbolic loop folding},
  booktitle    = {Programming - 34th European Symposium, {ESOP} 2025, Hamilton, Canada, May, 2025, Proceedings}, 
  series       = {Lecture Notes in Computer Science},
  volume       = {???},
  pages        = {??--??},
  publisher    = {Springer},
  year         = {2025},
  url          = {}, 
  doi          = {},
}