Extracting Program Logics From Abstract Interpretations Defined by Logical Relations

AbstractWe connect the activity of defining an abstract-interpretation-based static analysis with synthesizing its appropriate programming logic by applying logical relations as demonstrated by Abramsky. We begin with approximation relations of base type, which relate concrete computational values to their approximations, and we lift the relations to function space and upper- and lower-powerset. The resulting family's properties let us synthesize an appropriate logic for reasoning about the outcome of a static analysis. The relations need not generate Galois connections, but when they do, we show that the relational notions of soundness and completeness coincide with the Galois-connection-based notions