Practical applications of the Theory of Equality with Uninterpreted Functions (EUF)
Most automatic theorem provers handle EUF in some form. In particular, provers based on the Nelson-Oppen architecture do so. For big systems, however, EUF is usually not enough. One needs specialized decision procedures for arithmetic, arrays, bit vectors, and so on to get better performance. Take a look at SMT solvers. If you follow the links to solvers and where they are used you'll find many applications to real world problems. For example, Z3 is used in VCC, which in turn is used to fully verify Microsoft's (baby) hardware simulator Hyper-V.