Completeness in static analysis by abstract interpretation, a personal point of view

TL;DR

This paper discusses the concept of completeness in static analysis via abstract interpretation, highlighting practical issues and questions encountered in ensuring the analysis can infer true properties without false negatives.

Contribution

It provides a personal perspective on the challenges and considerations in achieving completeness in static analysis using abstract interpretation.

Findings

Highlights practical issues in achieving completeness

Raises questions about the limitations of static analysis

Provides insights from personal experience

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.