FDS task (Interprocedural, Finite, Distributive, Subsets) is well known compiler optimization technique which is applicable to sound, but not to precise source code static analysis. Evolution of symbolic execution methods applied to static inference of program execution facts can improve precision of program analysis.
This topic is devoted to an approach to program analysis which is both complete and precise and allows to detect security and stability problems in real-world projects in C and C++.