ETD

• abstract
• interpretation

This thesis investigates the ability to introduce a new variable in the novel LCL logic that combines under- and over-approximation. It outlines two new properties on the abstract domain as feasibility conditions, showing that they always hold on non-relational domains and proving the existence of relational domains for which they are not validated.