Nicolas Manini, PhD Student, IMDEA Software Institute
Abstract interpretation provides an over-approximation of program behaviours that is used to prove the absence of bugs. The ideal scenario for abstract interpretation is that of a complete analysis, where false alarms cannot arise. Unfortunately for any non-trivial abstract domain there is some program whose analysis is incomplete. In this talk we discuss an approach to characterizing classes of complete programs on some non-trivial abstract domains for studying their expressiveness. To this aim we present the notion of bounded domains and show the implications arising from the possibility of conducting a complete analysis on such domains. In the talk we show how to tackle the problems of deciding program termination and equivalence, and discuss applicability of our approach.