## 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

Publications

CSBNMC from proof-of-space [ Crypto 2019 ]

Fiat-Shamir: from practice to theory [ STOC 2019 ]

Traitor-tracing made simple and attribute-based [ TCC 2018 ]

GGH15 beyond permutation branching programs [ Crypto 2018 ]

Fiat-Shamir & CI from strong KDM-secure encryption [ Eurocrypt 2018 ]

Constraint-hiding constrained PRFs for NC1 from LWE [ Eurocrypt 2017 ]

Cryptanalyses of candidate branching program obfuscators [ Eurocrypt 2017 ]

Adaptive succinct garbled RAM, or how to delegate your database [ TCC 2016-B ]

On the correlation intractability of obfuscated pseudorandom functions [ TCC 2016-A ]

CSBNMC from proof-of-space [ Crypto 2019 ]

Fiat-Shamir: from practice to theory [ STOC 2019 ]

Traitor-tracing made simple and attribute-based [ TCC 2018 ]

GGH15 beyond permutation branching programs [ Crypto 2018 ]

Fiat-Shamir & CI from strong KDM-secure encryption [ Eurocrypt 2018 ]

Constraint-hiding constrained PRFs for NC1 from LWE [ Eurocrypt 2017 ]

Cryptanalyses of candidate branching program obfuscators [ Eurocrypt 2017 ]

Adaptive succinct garbled RAM, or how to delegate your database [ TCC 2016-B ]

On the correlation intractability of obfuscated pseudorandom functions [ TCC 2016-A ]