Completeness in static analysis by abstract interpretation, a personal point of view
Programming Languages
2024-12-11 v3
Abstract
Static analysis by abstract interpretation is generally designed to be "sound", that is, it should not claim to establish properties that do not hold-in other words, not provide "false negatives" about possible bugs. A rarer requirement is that it should be "complete", meaning that it should be able to infer certain properties if they hold. This paper describes a number of practical issues and questions related to completeness that I have come across over the years.
Cite
@article{arxiv.2211.09572,
title = {Completeness in static analysis by abstract interpretation, a personal point of view},
author = {David Monniaux},
journal= {arXiv preprint arXiv:2211.09572},
year = {2024}
}