Some decidability questions in abstract program semantics

This thesis explores program verification trough abstract interpretation in the context of computability theory. It explores the subject of analysis termination in the domain of intervals by presenting a novel approach in the design of the analyzer, which ensures convergence. The thesis also explores the same topic with general non relational collecting domains.