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.
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
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 ]