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.
- Did anyone use EUF to successfully solve real-world problems different than those indicated above?
- Did anyone use EUF to successfully solve the above problems, but in a real world setting rather than a toy setting?
- 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).