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.
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 senior research scientist 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 postdoc at EPFL. 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.