Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

David Monniaux

TL;DR

This paper examines how completeness in abstract interpretation can be achieved or limited in practice. It presents an exact abstraction for LRU caches, showing that a carefully composed abstraction and solving method can yield a unique, testable result, in contrast to brittle widening-based approaches. It then analyzes the sources of incompleteness—widening, imprecise transfer functions, and undecidability in richer domains—highlighting that complete methods (e.g., quantifier elimination or policy iteration) have predictable outcomes but often scalability issues. The discussion informs design choices for static analyzers by balancing completeness, precision, and performance, and suggests that complete methods are valuable for giving reproducible results in critical analyses such as WCET.

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.

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

TL;DR

This paper examines how completeness in abstract interpretation can be achieved or limited in practice. It presents an exact abstraction for LRU caches, showing that a carefully composed abstraction and solving method can yield a unique, testable result, in contrast to brittle widening-based approaches. It then analyzes the sources of incompleteness—widening, imprecise transfer functions, and undecidability in richer domains—highlighting that complete methods (e.g., quantifier elimination or policy iteration) have predictable outcomes but often scalability issues. The discussion informs design choices for static analyzers by balancing completeness, precision, and performance, and suggests that complete methods are valuable for giving reproducible results in critical analyses such as WCET.

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.
Paper Structure (12 sections, 2 equations, 1 figure)

This paper contains 12 sections, 2 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Completeness of the Abstraction: the Case of LRU Caches
  3. Completeness or Incompleteness of the Analysis Method
  4. Widening Operators
  5. Exact Solving
  6. Imprecise Abstract Transfer Functions
  7. Undecidability of an Abstraction
  8. Polyhedral Abstraction
  9. Undecidability with Quadratic Guards
  10. Perspectives and Dead Ends
  11. Richer Domains
  12. Perspectives and Conclusion

Figures (1)

  • Figure 1: When the process is non terminating, any polyhedron containing the reachable points inevitably goes below the parabola