In this work, we propose a static analysis by abstract interpretation for Robust CTL properties by taking advantage of our static analyzer FuncTion. A CTL property robustly hold if a controlled input imply it whatever the value of the uncontrolled input. Furthermore, we enhance Conflict Driven Analysis (CDA), an extension inspired by Conflict Driven Clause Learning from SMT-Solvers, aiming to refine termination analysis. CDA has been successfully implemented for all analyses supported in FuncTion, including CTL, guarantee, and recurrence analyses. These improvements are amalgamated to advance FuncTion implementation, which surpasses the capabilities of its previous version. Experimental evidence supporting the efficacy of these enhancements is also presented.
