CHUCHU FAN For beautiful eyes, look for the good in others; for beautiful lips, speak only words of kindness; and for poise, walk with the knowledge that you are never alone. --Audrey Hepburn

Welcome to Chuchu's homepage!

Welcome to Chuchu's homepage! You can also find my information at:

  • Department Profile at HERE
  • Google Scholar at HERE
  • DBLP at HERE
  • About me

    Image One I am Chuchu Fan, a fifth year graduate student in Professor Sayan Mitra's group and ECE department, UIUC. I also work closely with Professor Mahesh Viswanathan from the CS Department of UIUC. Before joining UIUC, I got my bachelor's degree from Tsinghua University, Department of Automation with honor.

    My research interests includes: Formal methods on Cyber-Physical Systems; Verification of Autonomous Driving; Formal Synthesis of Control Systems; Theoretical Computer Science; Game Theory.

    Check out our vefication and synthesis tool:
    • DryVR: a verification tool for black-box CPS
    • C2E2: a verification tool for CPS modeled as hybrid systems with differential equations
    • RealSyn: a synthesis tool for linear system with reach-avoid specification

    You can find my CV HERE.

    Recent News

    • RealSyn passed the CAV'18 Artifact Evaluation! Get a first glimpse of the tool HERE.
    • Feel thrilled to be selected for college of engineering's prestigious Mavis Future Faculty Fellowship, Class of 2018!
    • Three papers to appear at FLoC 2018 in July! One at CAV about controller synthesis, one at FM about approximate partial order reduction, and one at ADHS about verification of mixed-signal circuits. Preprints coming soon!
    • Got the Mac Van Valkenburg Research Award, April 2018
    • Check out our recent work on safety and risk analysis of autonomous and ADAS systems in IEEE Design and Test , January 2018
    • Spent a wonderful week at Heidelberg, Germany for the 5th Heidelberg Laureate Forum Program in September 2017

    Publications

    Verification, Synthesis and Reachability Theories

    Chuchu Fan, Umang Mathur, Sayan Mitra and Mahesh Viswanathan, Controller Synthesis Made Real: Reachavoid Specifications and Linear Dynamics, Computer-Aided Verification (CAV), 2018. [Link] [pdf] [Slides] [Artifact] (Arfifact Evaluated)
    @inproceedings{FanMMV:CAV2018,
      author = {Chuchu Fan and Umang Mathur and Sayan Mitra and Mahesh Viswanathan},
      title = {Controller Synthesis Made Real: Reachavoid Specifications and Linear Dynamics},
      booktitle = {Computer Aided Verification},
      pages = {347--366},
      year = {2018},
      publisher = {Springer International Publishing},
      url = {https://link.springer.com/chapter/10.1007%2F978-3-319-96145-3_19},
      doi = {10.1007/978-3-319-96145-3\_19}
    }
    Chuchu Fan, Zhenqi Huang and Sayan Mitra, Approximate Partial Order Reduction, International Symposium on Formal Methods (FM), 2018. [Link] [pdf] [Slides]

    The Arxiv version can be found at HERE

    @inproceedings{FanHM:FM2018,
      author = {Chuchu Fan and Zhenqi Huang and Sayan Mitra},
      title = {Approximate Partial Order Reduction},
      booktitle = {International Conference on Formal Methods (FM 2018)},
      pages = {588--607},
      year = {2018},
      publisher = {Springer},
      url = {https://link.springer.com/chapter/10.1007%2F978-3-319-95582-7_35},
      doi = {10.1007/978-3-319-95582-7_35}
    }
    Chuchu Fan, James Kapinski, Xiaoqing Jin and Sayan Mitra. Simulation-Driven Reachability Using Matrix Measures , ACM Transactions on Embedded Computing Systems (TECS), 2018. [Link] [pdf]
    @article{FanKJM:TECS18,
      author = {Chuchu Fan and James Kapinski and Xiaoqing Jin and Sayan Mitra},
      title = {Simulation-Driven Reachability Using Matrix Measures},
      journal = {{ACM} Trans. Embedded Comput. Syst.},
      volume = {17},
      number = {1},
      pages = {21:1--21:28},
      year = {2018},
      url = {https://dl.acm.org/citation.cfm?id=3126685},
      doi = {10.1145/3126685}
    }
    Chuchu Fan, Bolun Qi, Sayan Mitra and Mahesh Viswanathan, DRYVR:Data-driven verification and compositional reasoning for automotive systems , International Conference on Computer Aided Verification (CAV), 2017. [Link] [pdf] [Slides] [Talk Video] (Arfifact Evaluated)

    The ArXiv version can be found at HERE

    @inproceedings{FanQMV:CAV2017,
      author = {Chuchu Fan and Bolun Qi and Sayan Mitra and Mahesh Viswanathan},
      title = {DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems},
      booktitle = {Computer Aided Verification},
      pages = {441--461},
      year = {2017},
      publisher = {Springer International Publishing},
      crossref = {DBLP:conf/cav/2017-1},
      url = {https://link.springer.com/chapter/10.1007%2F978-3-319-63387-9_22},
      doi = {10.1007/978-3-319-63387-9_22}
    }
    Zhenqi Huang, Chuchu Fan and Sayan Mitra. Bounded invariant verification for time-delayed nonlinear networked dynamical systems, Nonlinear Analysis: Hybrid Systems (NAHS), 2017. [Link] [pdf]
    @article{HuangFM:NASH2017,
      title = {Bounded invariant verification for time-delayed nonlinear networked dynamical systems},
      journal = {Nonlinear Analysis: Hybrid Systems},
      volume = {23},
      pages = {211 - 229},
      year = {2017},
      issn = {1751-570X},
      doi = {https://doi.org/10.1016/j.nahs.2016.05.005},
      url ={http://www.sciencedirect.com/science/article/pii/S1751570X16300279},
      author = {Zhenqi Huang and Chuchu Fan and Sayan Mitra},
      keywords = {Compositional verification, Delayed dynamical systems, Simulation-based verification, Input-to-state stability}
    }
    Chuchu Fan, James Kapinski, Xiaoqing Jin and Sayan Mitra. Locally Optimal Reach Set Over-approximation for Nonlinear Systems , International Conference on Embedded Software (EMSOFT), 2016. (Best Paper Finalist). [Link] [pdf] [Slides]

    Full version report can be found at HERE

    @inproceedings{FanKJM:EMSOFT16,
      author = {Chuchu Fan and James Kapinski and Xiaoqing Jin and Sayan Mitra},
      title = {Locally optimal reach set over-approximation for nonlinear systems},
      booktitle = {2016 International Conference on Embedded Software, {EMSOFT} 2016, Pittsburgh, Pennsylvania, USA, October 1-7, 2016},
      pages = {6:1--6:10},
      year = {2016},
      url = {http://dl.acm.org/citation.cfm?id=2968482},
      doi = {10.1145/2968478.2968482}
    }
    Chuchu Fan and Sayan Mitra. Bounded Verification with On-the-fly Discrepancy Computation, International Symposium on Automated Technology for Verification and Analysis (ATVA), 2015. [Link] [pdf] [Slides]

    The Arxiv version can be found at HERE

    @inproceedings{FanM:ATVA2015,
      author = {Chuchu Fan and Sayan Mitra},
      title = {Bounded Verification with On-the-Fly Discrepancy Computation},
      booktitle = {Automated Technology for Verification and Analysis},
      pages = {446--463},
      year = {2015},
      url = {https://doi.org/10.1007/978-3-319-24953-7_32},
      doi = {10.1007/978-3-319-24953-7_32}
    }
    Huang, Zhenqi, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, and Marta Kwiatkowska. Invariant verification of nonlinear hybrid automata networks of cardiac cells, Computer-aided Verification (CAV), 2014. [Link] [pdf] [Slides]
    @inproceedings{HuangFMMK:CAV2014,
      author = {Zhenqi Huang and Chuchu Fan and Alexandru Mereacre and Sayan Mitra and Marta Z. Kwiatkowska},
      title = {Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells},
      booktitle = {Computer Aided Verification},
      pages = {373--390},
      year = {2014},
      url = {https://doi.org/10.1007/978-3-319-08867-9_25},
      doi = {10.1007/978-3-319-08867-9_25}
    }

    Verification Tools

    Bolun Qi, Chuchu Fan, Minghao Jiang, Sayan Mitra. DryVR 2.0: A tool for verification and controller synthesis of black-box cyber-physical systems nternational Conference on Hybrid Systems: Computation and Control (HSCC), 2018. [Link] [pdf]
    @inproceedings{QiFJM:HSCC2018,
      author = {Bolun Qi and Chuchu Fan and Minghao Jiang and Sayan Mitra},
      title = {DryVR 2.0: {A} tool for verification and controller synthesis of black-box cyber-physical systems},
      booktitle = {Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of {CPS} Week), {HSCC} 2018, Porto, Portugal, April 11-13, 2018},
      pages = {269--270},
      year = {2018},
      url = {http://doi.acm.org/10.1145/3178126.3187008},
      doi = {10.1145/3178126.3187008}
    }
    Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan and Parasara Sridhar Duggirala. Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2 , International Conference on Computer Aided Verification (CAV), 2016. [Link] [pdf] [Slides]
    @inproceedings{FanQMVD:CAV2016,
      author = {Chuchu Fan and Bolun Qi and Sayan Mitra and Mahesh Viswanathan and Parasara Sridhar Duggirala},
      title = {Automatic Reachability Analysis for Nonlinear Hybrid Models with {C2E2}},
      booktitle = {Computer Aided Verification - 28th International Conference, {CAV} 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part {I}},
      pages = {531--538},
      year = {2016},
      url = {https://doi.org/10.1007/978-3-319-41528-4_29}
    }

    Verification, Synthesis and Reachability Applications

    Chuchu Fan, Yu Meng, Jürgen Maier, Ezio Bartocci, Sayan Mitra and Ulrich Schmid, Verifying nonlinear analog and mixed-signal circuits with inputs, IFAC Conference on Analysis and Design of Hybrid Systems (ADHS), 2018. [Link] [pdf] [Models] [Slides]

    The Arxiv version can be found at HERE

    @inproceedings{FanMMBMS:ADHS2018,
      author = {Chuchu Fan and Yu Meng and J{\"{u}}rgen Maier and Ezio Bartocci and Sayan Mitra and Ulrich Schmid},
      title = {Verifying nonlinear analog and mixed-signal circuits with inputs},
      booktitle = {IFAC Conference on Analysis and Design of Hybrid Systems},
      pages = {},
      year = {2018},
      publisher = {},
      url = {},
      doi = {}
    }
    Chuchu Fan, Bolun Qi and Sayan Mitra. Data-driven formal reasoning and their applications in safety analysis of vehicle autonomy features , IEEE Design & Test, 2018. [Link] [pdf]
    @article{FanQM:IEEEDT2018,
      author={Chuchu Fan and Bolun Qi and Sayan Mitra},
      journal={{IEEE} Design {\&} Test},
      title={Data-Driven Formal Reasoning and Their Applications in Safety Analysis of Vehicle Autonomy Features},
      year={2018},
      volume={35},
      number={3},
      pages={31-38},
      doi={10.1109/MDAT.2018.2799804},
      ISSN={2168-2356},
      month={June},
      url = {http://ieeexplore.ieee.org/document/8272345/}
    }
    Md. Ariful Islam, Richard Defrancisco, Chuchu Fan, Radu Grosu, Sayan Mitra and Scott Smolka. Model Checking Tap Withdrawal in C. Elegans, Hybrid Systems Biology (HSB), 2015. Link
    Parasara Sridhar Duggirala, Chuchu Fan, Sayan Mitra, and Mahesh Viswanathan. Meeting a Powertrain Verification Challenge, Computer-aided Verification (CAV), 2015. [Link] [pdf] [Slides] (Artifact Evaluated)
    @inproceedings{DuggiralaFMV:CAV2015,
      author = {Parasara Sridhar Duggirala and Chuchu Fan and Sayan Mitra and Mahesh Viswanathan},
      title = {Meeting a Powertrain Verification Challenge},
      booktitle = {Computer Aided Verification},
      pages = {536--543},
      year = {2015},
      url = {https://doi.org/10.1007/978-3-319-21690-4_37},
      doi = {10.1007/978-3-319-21690-4_37}
    }
    Chuchu Fan, Parasara Sridhar Duggirala, Sayan Mitra, and Mahesh Viswanathan. Progress on Powertrain Verification Challenge with C2E2*, Applied Verification for Continuous and Hybrid Systems (ARCH), 2015 (Robert Bosch Best Verification Result). [Link] [pdf] [Slides]
    @inproceedings{FanDMV:ARCH2015,
      author = {Chuchu Fan and Parasara Sridhar Duggirala and Sayan Mitra and Mahesh Viswanathan},
      title = {Progress on Powertrain Verification Challenge with {C2E2}},
      booktitle = {1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems, ARCH@CPSWeek 2014, Berlin, Germany, April 14, 2014 / ARCH@CPSWeek 2015, Seattle, WA, USA, April 13, 2015.},
      pages = {207--212},
      year = {2015},
      rl = {http://www.easychair.org/publications/paper/248666}
    }
    Huang, Zhenqi, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, and Marta Kwiatkowska. Simulation-based Verification of Implantable Medical Devices with Guaranteed Coverage, IEEE Design & Test, 2015. [Link] [pdf]
    @article{HuangFMMK:IEEEDT2015,
      author = {Zhenqi Huang and Chuchu Fan and Alexandru Mereacre and Sayan Mitra and Marta Z. Kwiatkowska},
      title = {Simulation-Based Verification of Cardiac Pacemakers With Guaranteed Coverage},
      journal = {{IEEE} Design {\&} Test},
      volume = {32},
      number = {5},
      pages = {27--34},
      year = {2015},
      url = {https://doi.org/10.1109/MDAT.2015.2448543},
      doi = {10.1109/MDAT.2015.2448543}
    }

    Machine Learning and Image Processing

    Qiang Ning, Zhongzhi Yu, Chuchu Fan, and Dan Roth, Exploiting Partially Annotated Data in Temporal Relation Extraction, The Joint Conference on Lexical and Computational Semantics (*SEM), 2018. [Link] [pdf]
    @inproceedings{NingYuFaRo:SEM18,
      author = {Qiang Ning and Zhongzhi Yu and Chuchu Fan and Dan Roth},
      title = {Exploiting Partially Annotated Data for Temporal Relation Extraction},
      booktitle = {The Joint Conference on Lexical and Computational Semantics (*SEM)},
      month = {6},
      year = {2018},
      publisher = {Association for Computational Linguistics},
      url = {http://cogcomp.org/papers/NingYuFaRo18.pdf}
    }
    Qiang Ning, Kan Chen, Li Yi, Chuchu Fan, Yao Lu, Jiangtao Wen, Image Super-Resolution via Analysis Sparse Prior, IEEE Signal Processing Letters, 2013. [Link] [pdf]
    @article{NingCYFLW:IEEESPL13,
      author = {Qiang Ning and Kan Chen and Li Yi and Chuchu Fan and Yao Lu and Jiangtao Wen},
      title = {Image Super-Resolution Via Analysis Sparse Prior},
      journal = {{IEEE} Signal Process. Lett.},
      volume = {20},
      number = {4},
      pages = {399--402},
      year = {2013},
      url = {https://doi.org/10.1109/LSP.2013.2242198},
      doi = {10.1109/LSP.2013.2242198}
    }

    Tutorial

    Parasara Sridhar Duggirala, Chuchu Fan, Matthew Potok, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Stanley Bak, Sergiy Bogomolov, Taylor T. Johnson, Luan Viet Nguyen, Christian Schilling, Andrew Sogokon, Hoang-Dung Tran, Weiming Xiang: Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP, IEEE Conference on Control Applications(CCA), 2016. [Link] [pdf]
    @inproceedings{DBLP:conf/IEEEcca/DuggiralaFPQM0B16,
      author = {Parasara Sridhar Duggirala and Chuchu Fan and Matthew Potok and Bolun Qi and Sayan Mitra and Mahesh Viswanathan and Stanley Bak and Sergiy Bogomolov and Taylor T. Johnson and Luan Viet Nguyen and Christian Schilling and Andrew Sogokon and Hoang{-}Dung Tran and Weiming Xiang},
      title = {Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP},
      booktitle = {2016 {IEEE} Conference on Control Applications, {CCA} 2016, Buenos Aires, Argentina, September 19-22, 2016},
      pages = {1024--1029},
      year = {2016},
      url = {https://doi.org/10.1109/CCA.2016.7587948},
      doi = {10.1109/CCA.2016.7587948}
    }

    Patents

    Sayan Mitra, Chuchu Fan and Zhenqi Huang, Bounded verification through discrepancy computations, United States Patent Application 20160179999. [Link]
    Qiang Ning, Kan Chen, Li Yi, Chuchu Fan, Yao Lu and Jiangtao Wen, Image Super-Resolution via Analysis Sparse Prior, China patent 2012105247162. [Link]

    Contact Info.

    Address: 247 CSL,  1308 W Main St,  Urbana,  IL,  61801
    Email (school): cfan10 at illinois dot edu
    Website: chuchufan.info