CVC4

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

About
News
Downloads
Documentation
Publications
Awards
People
History
Third-Party Applications
Acknowledgements

Try CVC4 online!


People

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.

Senior Technical Leads

Haniel Barbosa (Universidade Federal de Minas Gerais)

Aina Niemetz (Stanford University)

Mathias Preiner (Stanford University)

Andrew Reynolds (University of Iowa)

Current Developers

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

Ahmed Irfan (Stanford University)

Gereon Kremer (Stanford University)

Makai Mann (Stanford University)

Abdalrhman Mohamed (University of Iowa)

Mudathir Mohamed (University of Iowa)

Andres Nötzli (Stanford University, Amazon)

Alex Ozdemir (Stanford University)

Ying Sheng (Stanford University)

Yoni Zohar (Stanford University)