Lexical and numerical domains for abstract interpretation

The goal of this thesis is to contribute to the field of formal methods employed for the static verifi cation of computer program properties. The context is the Abstract Interpretation framework, one of the various possible techniques to perform static analyses. In particular, we focus on the design of novel abstract domains to analyze the basic building blocks of computer programs: lexical and numerical variables, as well as relationships between variables. In order to provide experimental evidence of their actual applicability, we implemented our domains and we applied them to a suite of case studies.