Complete instantiation for quantified formulas in satisfiabiliby modulo theories Y Ge, L De Moura International Conference on Computer Aided Verification, 306-320, 2009 | 258 | 2009 |

Solving quantified verification conditions using satisfiability modulo theories Y Ge, C Barrett, C Tinelli International Conference on Automated Deduction, 167-182, 2007 | 91 | 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 | 77 | 2006 |

Instantiation-based invariant discovery T Kahsai, Y Ge, C Tinelli NASA Formal Methods Symposium, 192-206, 2011 | 42 | 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 | 39 | 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 | 11 | 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 | 1 | 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 | | |