The essence of abstract interpretation lies in the use of a simplified domain of abstract properties, known as the abstract domain, which enables the proof of properties about the concrete semantics of programs in a computationally feasible manner. In this seminar, I will demonstrate that certain elements within the concrete domain, called generators, play a crucial role in analyzing the precision (i.e., completeness) and the bounded imprecision (i.e., partial completeness) of a Galois connection-based abstract interpretation. In particular, I will show that when the underlying Galois connection satisfies a structural property on generators, the precision and bounded imprecision of an abstract interpretation are entirely determined by its behavior on generators.
