Practical applications of the Theory of Equality with Uninterpreted Functions (EUF)

Question

In these days I'm reading the book Decision Procedures - An Algorithmic Point of View. Chapters 3 and 4 deal with the Theory of Equality with Uninterpreted Functions (EUF). The authors give 3 toy examples on using EUF to solve real-world problems: proving equivalence of programs, proving equivalence of circuits, validating the translation performed by a compiler. I'm looking for further practical applications of EUF, possibly non-toy examples.

Question(s)

1. Did anyone use EUF to successfully solve real-world problems different than those indicated above?
2. Did anyone use EUF to successfully solve the above problems, but in a real world setting rather than a toy setting?
3. Did anyone use EUF to model (parts of) big, complex systems? What did you model? What did you manage to prove about such systems? Do you have any success story to tell?

Pointers to papers are greatly appreciated. I've already posted this question on ai.stackexchange.com, without receiving any answer (moreover, unfortunately that site was closed during its beta for insufficient activity).

Answer 1

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.

Answer 2

Radu's answers is great! To add some more context:

Depending on what you want to do, in addition to decision procedures you may also need quantifier instantiation. In particular, background axiomatization as well as user supplied specifications of the Hyper-V rely heavily on quantified formulas.

There are other users of Z3, whom you may consider more real world. For example, Patrice Godefroid’s SAGE is used in a huge fuzzing server farm used to find bugs in file parsers at Microsoft.