Sicun (Sean) Gao
Computer Science Department
Carnegie Mellon University
Technical Coordinator of CMACS (NSF Expedition in Computing)
Email: sicung at cs dot cmu dot edu
Office: Gates-Hillman Center 9004
CV: [pdf] (last updated: November 12, 2013)
I combine logical/algebraic/numerical approaches to develop automated and reliable methods for solving real-world engineering problems, especially for the design/verification/implementation/security of cyber-physical systems.
- dReal. An open-source SMT solver for nonlinear theories over the reals, allowing transcendental functions and differential equations. It has scaled on formulas with hundreds of nonlinear ODEs. Available here.
- dReach. An open-source tool for reachability analysis of nonlinear hybrid systems using bounded model checking and invariant-based reasoning. Available here.
- Cerifying floating-point computation in GNU C Library. Produce formal proofs or report bugs for standard numerical routines. Many serious bugs are found. For instance, in rounding mode FE_UPWARD, sin(0.851600)=1489379514151358920516113347498016545730127812624384.0, when compiled with gcc (eglibc-2.14) in Ubuntu 12.04 LTS on Intel cores.
- Automotive systems. Verify autonomous driving systems being developed at the
GM-CMU Collaborative Lab.
- Biological systems. Automated analysis and control design for complex biological models in atrial fibrillation, prostate cancer, etc.
- Model-based robot design and implementation. A framework for solver-aided controller design and automatic code-generation. Currently used for building a two-wheeled robot from scratch with formal assurance of safety properties.
- Complex models from safety-critical applications. Rigorous analysis of realistic flight-control models and power-system models.
- Delta-Complete Reachability Analysis (Part I). Sicun Gao, Soonho Kong, and Edmund Clarke. CMU SCS Technical Report CMU-CS-13-131.
- Floating-Point Bugs in the Embedded GNU C Library. Soonho Kong, Sicun Gao, and Edmund Clarke. CMU SCS Technical Report CMU-CS-13-130. [pdf]
- Satisfiability Modulo ODEs. Sicun Gao, Soonho Kong, and
Edmund Clarke. In FMCAD (Formal Methods in Computer-Aided Design)
- Extracting Proofs from Branch-and-Prune. Sicun Gao, Soonho
Kong, and Edmund Clarke. CMU SCS Technical Report CMU-CS-13-104.
- 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.
(CMU School of Computer Science Distinguished Dissertation Award Honorable Mention)
- 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. [pdf] [arXiv]
- Delta-Decidability over the Reals. Sicun Gao, Jeremy
Avigad, and Edmund Clarke. In LICS (Logic in Computer Science) 2012.
- 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 in 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. Committee: Edmund Clarke,
Jeremy Avigad, and Andre Platzer. [pdf]
- 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