Deciding Program Properties via Complete Abstractions on Bounded Domains

Abstract interpretation provides an over-approximation of program behaviours that is used to prove the absence of bugs. When the computed approximation in the chosen abstract domain is as precise as possible, we say the analysis is complete and false alarms cannot arise. Unfortunately for any non trivial abstract domain there is some program whose analysis is incomplete. In this paper we want to characterize the classes of complete programs on some non-trivial abstract domains for studying their expressiveness. To this aim we introduce the notion of bounded domains for posets with ascending chains of bounded length only. We show that any complete program on bounded domains can be rewritten in an equivalent canonical form without nontrivial loops. This result proves that program termination on the class of complete programs on bounded domain is decidable. Moreover, semantic equivalence between programs in the above class can be reduced to determining the equivalence of a set of guarded statements. We show how our approach can be applied to a quite large class of programs. Indeed, abstract domains defined on Boolean abstractions that are complete for the same functions can be composed by preserving boundedness and completeness also w.r.t. any expressible guard. This suggests that new complete bounded abstract domains can be tailored on the guards and functions appearing in the program. Their existence is sufficient to prove decidability of termination and program equivalence for such programs.