Complete instantiation for quantified formulas in satisfiabiliby modulo theories Y Ge, L De Moura Computer Aided Verification: 21st International Conference, CAV 2009 …, 2009 | 312 | 2009 |
Solving quantified verification conditions using satisfiability modulo theories Y Ge, C Barrett, C Tinelli Automated Deduction–CADE-21: 21st International Conference on Automated …, 2007 | 94 | 2007 |
Cooperating theorem provers: A case study combining HOL-Light and CVC Lite S McLaughlin, C Barrett, Y Ge Electronic Notes in Theoretical Computer Science 144 (2), 43-51, 2006 | 75 | 2006 |
Instantiation-based invariant discovery T Kahsai, Y Ge, C Tinelli NASA Formal Methods Symposium, 192-206, 2011 | 46 | 2011 |
Solving quantified verification conditions using satisfiability modulo theories Y Ge, C Barrett, C Tinelli Annals of Mathematics and Artificial Intelligence 55 (1), 101-122, 2009 | 44 | 2009 |
Proof translation and SMT-LIB benchmark certification: A preliminary report Y Ge, C Barrett SMT 2008: 6th International Workshop on Satisfiability Modulo Theories, 33, 2008 | 18 | 2008 |
Comparing proof systems for linear real arithmetic with LFSC A Reynolds, L Hadarean, C Tinelli, Y Ge, A Stump, C Barrett International Workshop on Satisfiability Modulo Theories, 2010 | 12 | 2010 |
Complete instantiation for quantified SMT formulas Y Ge, L de Moura CAV 5643, 2009 | 11 | 2009 |
Cvc3 proof conversion to lfsc A Reynolds, C Tinelli, A Stump, L Hadarean, Y Ge, C Barrett Technical Report, 2010 | 2 | 2010 |
Solving quantified first order formulas in Satisfiability Modulo Theories Y Ge New York University, 2010 | | 2010 |
From Declarative to Computational Proof Checking for LRA A Reynolds, L Hadarean, C Tinelli, Y Ge, A Stump, C Barrett | | |