People

Project Leaders

I am an assocate professor at NYU 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.

Developers

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.

As a postdoc at NYU, I have worked on many parts of CVC4.  My most notable contributions to the current codebase are the expression package, compatibility library, language bindings, SMT-LIB compliance, much of the parser and printing framework, the public API, and the build system.  I've worked on several preprocessing passes as well.

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 am a PhD student working with Clark at NYU.  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 Phd Student at the University of Iowa.  My research focus has been handling quantified formulas in SMT.  In CVC4, I have implemented both a variation of E-matching for finding unsatisfiable instances, as well as a finite model finding procedure for finding satisfiable instances.  I also wrote the datatypes theory solver and contributed to the core model generation procedure.