(Sicun|Sean) Gao


PhD Student in Pure and Applied Logic
Carnegie Mellon University

Advisors
Prof. Edmund Clarke (Dept of Computer Science and Electrical Engineering)
Prof. Jeremy Avigad (Dept of Philosophy and Mathematics)

Interests
I study logical/algebraic/numerical methods to formally analyze complex systems (cyber-physical, biological, etc.; see the CMACS project), with a focus on developing decision algorithms for nonlinear first-order theories over reals and finite fields.
Papers
Delta-Complete Reachability Analysis of Hybrid Systems
with Jeremy Avigad and Edmund Clarke
In Preparation

Delta-Complete Decision Procedures for Satisfiability over the Reals
Sicun Gao, Jeremy Avigad, and Edmund Clarke
Submitted [pdf]

Delta-Decidability over the Reals
Sicun Gao, Jeremy Avigad, and Edmund Clarke
Submitted [pdf]

Quantifier Elimination over Finite Fields with Groebner Bases
Sicun Gao, Andre Platzer, and Edmund Clarke
In CAI (International Conference on Algebraic Informatics) 2011 [pdf] [arXiv]

Integrating ICP and LRA Solvers for Deciding Nonlinear Real Arithmetic
Sicun Gao, Malay Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan, and Edmund Clarke
In FMCAD (Formal Methods for Computer Aided Design) 2010 [pdf]

A Non-Prenex DPLL-Based QBF Solver with Game-State Learning
William Klieber, Samir Sapra, Sicun Gao, and Edmund Clarke
In SAT (Theory and Applications of Satisfiability Testing) 2010 [pdf]

Counting Zeros over Finite Fields with Groebner Bases
MS Thesis in Logic and Computation [pdf]
Committee: Edmund Clarke, Jeremy Avigad, and Andre Platzer

Background
BS in Mathematical Logic
BS in Mathematics
Peking University, Beijing, China (2006)
Contact
sicung AT cs DOT cmu DOT edu
9232 Gates-Hillman Center/135 Baker Hall, Carnegie Mellon University, Pittsburgh, PA 15213

The infinite we shall do right away. The finite may take a little longer. -- Stanislaw Ulam