Complete Abstractions Everywhere

摘要

While soundness captures an essential requirement of the intrinsic approximation of any static analysis, completeness encodes approximations that are as precise as possible. Although a static analysis of some undecidable program property cannot be complete relatively to its reference semantics, it may well happen that it is complete relatively to an approximated and decidable reference semantics. In this paper, we will argue on the ubiquity of completeness properties in static analysis and we will discuss the beneficial role that completeness can play as a tool for designing and fine-tuning static analyses by reasoning on the completeness properties of their underlying abstract domains.