An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Third-Party Applications

Try CVC4 online!


Project Leaders

Clark Barrett (Stanford University)
I am a professor at Stanford University and a project leader for CVC4. I work with all of the developers closely and have contributed code for a variety of features, including the array theory solver, several preprocessing phases, parts of the combination framework, and the model generation procedure.

Cesare Tinelli (University of Iowa)
I’m a Professor of Computer Science at the University of Iowa and a project leader for CVC4. I’m involved mainly in high level activities such as overall design and new features and algorithms, and in the research behind them. I’m also active in seeking and securing funding for CVC4’s development from governmental agencies and through collaborations with industrial partners.

Current Developers

Haniel Barbosa (Universidade Federal de Minas Gerais)

Martin Brain (University of Oxford and City University of London)

Ahmed Irfan (Stanford University)

Makai Mann (Stanford University)

Aina Niemetz (Stanford University)

Andres Nötzli (Stanford University)

Alex Ozdemir (Stanford University)

Mathias Preiner (Stanford University)

Andrew Reynolds (University of Iowa)

Yoni Zohar (Stanford University)