(Sicun|Sean) Gao
Postdoctoral Researcher
Computer Science Department
Carnegie Mellon University
Email: sicung at cs dot cmu dot edu
Office: Gates-Hillman Center 9004
Interests
I develop logical/algebraic/numerical methods to automate the analysis and design of complex systems.
Papers
Delta-Reachability of Hybrid Systems
Sicun Gao, Soonho Kong, and Edmund Clarke
Submitted
Satisfiability Modulo ODEs Revisited
Sicun Gao, Soonho Kong, and Edmund Clarke
Submitted
Extracting Proofs from Branch-and-Prune
Sicun Gao, Soonho Kong, and Edmund Clarke
Submitted
dReal: An SMT Solver for Nonlinear Theories of Reals
Sicun Gao, Soonho Kong, and Edmund Clarke
In CADE (International Conference on Automated Deduction) 2013 [pdf] [tool]
Computable Analysis, Decision Procedures, and Hybrid Automata: A New Framework for the Formal Verification of Cyber-Physical Systems
PhD Thesis
Committee: Edmund Clarke (co-chair), Jeremy Avigad (co-chair), Lenore Blum, Randy Bryant, and Jeannette Wing
Delta-Complete Decision Procedures for Satisfiability over the Reals
Sicun Gao, Jeremy Avigad, and Edmund Clarke
In IJCAR (International Joint Conference on Automated Reasoning) 2012 [arXiv]
Delta-Decidability over the Reals
Sicun Gao, Jeremy Avigad, and Edmund Clarke
In LICS (Logic in Computer Science) 2012 [arXiv]
Quantifier Elimination over Finite Fields with Groebner Bases
Sicun Gao, Andre Platzer, and Edmund Clarke
In CAI (International Conference on Algebraic Informatics) 2011 [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
Software
dReal: An SMT Solver for
Nonlinear Theories of the Reals
dReach: Reachability Analysis for Nonlinear Hybrid Systems
Background
PhD in Logic, Carnegie Mellon University (2012)
BS in Logic and BS in Mathematics, Peking University (2006)
The infinite we shall do right away. The finite may take a little longer. -- Stanislaw Ulam
