## Integrating SMT-Solvers: CVC4 and Alt-Ergo

**Participants:**Yilei Chen and Sachin Vasant

**Course information:**CS512 - Formal Method

**Project description:**In this project, we aim to achieve the following:

- Characterize and compare the power of the CVC4 and Alt-Ergo SMT solvers.

- To elaborate, we aim to identify a domain of formulae/lemmas (possibly a part of one or more theories), for which we compare the solving powers of the two SMT solvers, i.e., does each of the solver recognize and solve such formulae /lemmas, do the solvers allow proof my induction, etc.

- Come up with an SMT solver for the domain by integrating the aforementioned SMT solvers. Hence, the final solver must be more powerful and if possible more efficient than these solvers individually.

**Description of SMT-LIB, CVC4, Alt-Ergo**

Introduction, and outline of the Theories they are supporting, see more

**Compare CVC4 with Alt-Ergo**

Through Theory compatibility, Performances on Logics. Click here for the details

**Towards Integrating**

To see how our integrator works click here