Documentation
- C2E2 User’s Guide (ver 2.1) 2020 (November 5)
- C2E2 User’s Guide (ver 2.0) 2018
- C2E2 User’s Guide (ver 1.0). Modified by Fan, Qi. 2016
- C2E2 User’s Guide Old. Duggirala, Mitra, Viswanathan, and Potok. 2014.
Publications, Tech Reports, and Preprints
- ARCH report on hybrid verification (Coming soon!)
- A technique for verifying nonlinear analog and mixed-signal circuits with inputs. Chuchu Fan, Yu Meng, Jürgen Maier, Ezio Bartocci, Sayan Mitra, Ulrich Schmid. In proceedings of ADHS, Oxford, UK, FloC 2018.
- Automatic Reachability Analysis for Nonlinear Hybrid Models with C2E2. Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Parasara Sridhar Duggirala, Computer Aided Verification CAV (1), 531-538, 2016.
-
Locally optimal reach set over-approximation for nonlinear systems.Chuchu Fan, James Kapinski, Xiaoqing Jin, and Sayan Mitra: ACM SIGBED Conference on Embedded Software (EMSOFT 2016): 6:1-6:10, 2016.
- Meeting a Powertrain Verification Challenge. Duggirala, Fan, Mitra & Viswanathan. In CAV 2015 (Presents the results of applying simulation based verification algorithm described in C2E2, along with novel ways of computing discrepancy function on powertrain control system)
- Progress on Powertrain Verification Challenge with C2E2*. Fan, Duggirala, Mitra & Viswanathan. 2nd Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH) conducted as a part of CPS Week 2015. (Won the Most Promising Benchmark Results Prize sponsored by Robert Bosch GmbH).
- C2E2: A Verification Tool For Stateflow Models. Duggirala, Mitra, Viswanathan & Potok. TACAS 2015. (Describes the algorithm for general nonlinear hybrid systems with invariants and guards; describes some key aspects of the tool C2E2.)
- Bounded Verification with On-the-Fly Discrepancy Computation. Chuchu Fan & Sayan Mitra. Coordinated Science Laboratory technical report UILU-ENG-15-2201, University of Illinois at Urbana-Champaign, February 2015. (Describes a new algorithm for computing discrepancy function automatically. New feature implemented in current release.)
-
Bounded Verification with On-the-Fly Discrepancy Computation. Chuchu Fan and Sayan Mitra: Automated Technology for Verification and Analysis (ATVA 2015): 446-463, 2015.
- Verification of Annotated Models from Executions. Duggirala, Mitra & Viswanathan. EMSOFT 2013. (Describes algorithm for nonlinear and switched models.)
- Temporal Precedence Checking for Switched Models and its Application to a Parallel Landing Protocol. Duggirala, Wang, Mitra, Munoz & Viswanathan, Formal Methods 2014. (Describes algorithm for verifying temporal properties and applies it to verify important properties of parallel landing protocol. Not in current release.)
- Invariant Verification of Nonlinear Hybrid Automata Networks of Cardiac Cells. Huang, Fan, Mereacre, Mitra & Kwiatkowska. CAV 2014. (Describes compositional analysis with simulations. Not in current release.)