Yeting Ge Ph.D. Department of Computer Science New York University Email: yeting at cs nyu edu

Research

My research interests are formal methods and automated theorem proving. My PhD advisor is Clark Barrett.

Personal

I defended my dissertation in November 2009. After that I was a postdoctoral scholar at University of Iowa, working with Cesare Tinelli. Since September 2010, I work for a company called Two Sigma in SoHo.

Recent Papers

• Yeting Ge and Leonardo de Moura. Complete Instantiation of Quantified Formulas in Satisfiability Modulo Theories. Proceedings of the 21th International Conference on Computer Aided Verification (CAV 2009),pages 306-320. Springer, 2009. Grenoble, France.

• Yeting Ge, Clark Barrett, and Cesare Tinelli. Solving Quantified Verification Conditions using Satisfiability Modulo Theories. Annals of Mathematics and Artificial Intelligence, 55(1), 2009.

• Yeting Ge and Clark Barrett. Proof Translation and SMT-LIB Benchmark Certification: A Preliminary Report. Extended abstract, 6th International Workshop on Satisfiability Modulo Theories, August 2008, Princeton, New Jersey.

• Yeting Ge, Clark Barrett, and Cesare Tinelli. Solving Quantified Verification Conditions using Satisfiability Modulo Theories. In Frank Pfenning, editor, Proceedings of the 21st International Conference on Automated Deduction (CADE 21), volume 4603 of Lecture Notes in Artificial Intelligence, pages 167-182. Springer-Verlag, July 2007. Bremen, Germany.

• Sean McLaughlin, Clark Barrett, and Yeting Ge. Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. In Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR '05), volume 144(2) of Electronic Notes in Theoretical Computer Science, pages 43-51. Elsevier, January 2006. Edinburgh, Scotland.

Slides

• Complete Instantiation for Quantified Formulas in Satisfiability Modulo Theories, SMT 2009, August 2009, Montreal, Canada

• Complete Instantiation for Quantified Formulas in Satisfiability Modulo Theories, ACSys seminar, December 2008, NYU

• Proof Translation and SMT-LIB Benchmark Certification: A Preliminary Report, SMT 2008, July 2008, Princeton

• Proof translation from CVC3 to HOL Light, ACSys seminar, March 2008, NYU

• Proofs from SAT solvers, ACSys seminar, November 2007, NYU

• Solving Quantified Verification Conditions using Satisfiability Modulo Theories, CADE 21, July 2007, Bremen, Germany

• Solving Quantified Verification Conditions using Satisfiability Modulo Theories, Third Northeastern Verification Seminar, May 2007, Princeton, NJ

• Difference logic, UTVPI and SLICE, ACSys seminar, October 2006, NYU