A calculus of logical relations for over- and underapproximating static analyses

Motivated by Dennis Dams’ studies of over- and underapproximation of state-transition systems, we define a logical-relation calculus for Galois-connection building. The calculus lets us define overapproximating Galois connections in terms of lower powersets and underapproximating Galois connections in terms of upper powersets. Using the calculus, we synthesize Dams’ most-precise over- and underapproximating transition systems and obtain proofs of their soundness and best precision as corollaries of abstract-interpretation theory. As a bonus, the calculus yields a logic that corresponds to the variant of Hennessy–Milner logic used in Dams’ results. Following from a corollary, we have that Dams’ most-precise approximations soundly validate most properties that hold true for the corresponding concrete system. These results bind together abstract interpretation and abstract model checking, as intended by Dams.