Project Leaders

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.

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.


I am a PhD student at NYU. I have worked on the portfolio (parallel) driver and branching heuristics in CVC4.

I'm a Researcher, at the Commissariat à l'Energie Atomique (CEA). I have worked on the rewrite rules theory.

I am a software engineer at Google. I am responsible for CVC4's parsing framework and for its complete lack of bugs.

I am Ph.D. student at New York University working with Clark Barrett. On CVC4 I worked on an early prototype for the array theory solver, the proof generating code and I am currently working on the bit-vector theory solver.

I am a computer scientist at SRI. My main contributions to CVC4 are the Boolean search engine (incorporating the minisat SAT solver), an efficient equality and congruence  reasoning engine, and the theory combination framework.

I did my PhD with Clark at NYU. I am currently at Verimag working as a Research Scientist. Most of the code in CVC4's arithmetic solver can be blamed on me.

I'm a PhD Student with Cesare Tinelli at the University of Iowa. My research focuses on parallel theorem proving. In CVC4, I'm working on the theory of Rewriting Rule and the theory of String.

I'm a research scientist at University of Iowa.  My research focus has been various approaches for quantified formulas in SMT, including E-matching, finite model finding, and techniques for automating induction.  I also wrote the datatypes theory solver and co-wrote the strings theory solver.

Fork me on GitHub