<p>Most automatic theorem provers handle EUF in some form. In particular, provers based on the <a href="http://scholar.google.co.uk/scholar?cluster=18185855484888710358">Nelson-Oppen</a> 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 <a href="http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories">SMT solvers</a>. If you follow the links to solvers and where they are used you'll find <em>many</em> applications to real world problems. For example, Z3 is used in <a href="http://research.microsoft.com/en-us/projects/vcc/">VCC</a>, which in turn is used to fully verify Microsoft's (baby) hardware simulator Hyper-V.</p>

CC BY-SA 2.5
2011-01-17T15:13:41.793Z
2011-01-17T15:13:41.793Z
Radu GRIGore
<p>Radu's answers is great! To add some more context:</p>

<p>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.</p>

<p>There are other users of Z3, whom you may consider more real world. For example, <a href="http://research.microsoft.com/en-us/um/people/pg/" rel="nofollow">Patrice Godefroid’s</a> SAGE is used in a huge fuzzing server farm used to find bugs in file parsers at Microsoft.</p>

CC BY-SA 2.5
2011-01-20T22:08:09.590Z
2011-01-20T22:08:09.590Z
Michal Moskal
<p>In these days I'm reading the book <a href="http://www.decision-procedures.org">Decision Procedures - An Algorithmic Point of View</a>. Chapters 3 and 4 deal with the <a href="http://www.decision-procedures.org/slides/uf.pdf">Theory of Equality with Uninterpreted Functions (EUF)</a>. 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.</p>

<blockquote>
  <p><strong>Question(s)</strong>  </p>
  
  <ol><li>Did anyone use EUF to successfully solve real-world problems different than those indicated above?</li>
  <li>Did anyone use EUF to successfully solve the above problems, but in a real world setting rather than a toy setting?</li>
  <li>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?</li></ol>
</blockquote>

<p>Pointers to papers are greatly appreciated. I've already posted this question on <a href="http://ai.stackexchange.com">ai.stackexchange.com</a>, without receiving any answer (moreover, unfortunately that site was closed during its beta for insufficient activity).</p>

<reference-request><lo.logic><ai.artificial-intel><software><application-of-theory>
Practical applications of the Theory of Equality with Uninterpreted Functions (EUF)
Giorgio Camerani
# Practical applications of the Theory of Equality with Uninterpreted Functions (EUF)

(Asked by: username_0 on 2011-01-17)

In these days I'm reading the book [Decision Procedures - An Algorithmic Point of View](http://www.decision-procedures.org). Chapters 3 and 4 deal with the [Theory of Equality with Uninterpreted Functions (EUF)](http://www.decision-procedures.org/slides/uf.pdf). 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](http://ai.stackexchange.com), without receiving any answer (moreover, unfortunately that site was closed during its beta for insufficient activity).

**Tags:** reference-request, lo.logic, ai.artificial-intel, software, application-of-theory


---

## 2 answers

### Answer by username_1 on 2011-01-17. Score: 8

Most automatic theorem provers handle EUF in some form. In particular, provers based on the [Nelson-Oppen](http://scholar.google.co.uk/scholar?cluster=18185855484888710358) 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](http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories). 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](http://research.microsoft.com/en-us/projects/vcc/), which in turn is used to fully verify Microsoft's (baby) hardware simulator Hyper-V.


---

### Answer by username_2 on 2011-01-20. Score: 3

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](http://research.microsoft.com/en-us/um/people/pg/) SAGE is used in a huge fuzzing server farm used to find bugs in file parsers at Microsoft.


---

