VEX is designed and widely used in dynamic analysis, in the form of Valgrind. Barring some implementation issues, VEX's side-effects-free, mostly-architecture-independent implementation provides an effective base on which to build non-dynamic analyses, as well. Specifically, we have used VEX to implement architecture-independent static and symbolic analyses.

Symbolic analysis is an active area of research, and many challenges are faced when attempting to implement it. These challenges include tradeoffs between tractability and precision when reasoning about symbolic memory, the NP-completeness of the underlying SMT-solving algorithms, difficult-to-analyze program actions, and many others. Some of these challenges are unsolveable, but compromises can be made to achieve useful results with symbolic analysis. This talk attempts to outline these challenges, describe some solutions, and provide a guide for parties interested in symbolic analysis with VEX.