Deciding program properties via complete abstractions on bounded domains

Abstract interpretation is very useful for program analysis, because it provides a (sound) over-approximation of program behaviours. When such approximation is as precise as possible in the current abstract domain, we say the analysis is complete, which is the best possible scenario for the analysis. Unfortunately it has been shown that whenever the programming language is Turing equivalent, then only trivial abstract domains are complete for all programs. Therefore, given a non-trivial abstract domain, we want to characterize the classes of complete programs on that domain and which is the expressiveness of such complete programs. To this aim, in this thesis we introduce the notion of bounded domains to denote posets admitting ascending chains of bounded length only and restrict our attention to investigate the expressiveness of programs for which the analysis is complete. The first result is that any complete program on bounded domains can be rewritten in an equivalent canonical form without nontrivial loops. This result enables us to conclude that program termination is decidable and gives an effective approach to solve it. As a second result, we show that the semantic equivalence between any two programs can be reduced to determining equivalence between sets of guarded statements