(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