About

Compare Execute Check Engine (C2E2) is a tool for verifying hybrid automata. Hybrid automata are models combining finite state machines and differential equations. They are used for modeling and analyzing robots, autonomous cars, medical devices—more generally, dynamical systems controlled by software. C2E2 can automatically check bounded time invariant properties of nonlinear hybrid automata. The new C2E2 (ver 2.0, Sept 2018) supports compositional modeling, nonlinear dynamics, model editing, and has a powerful new plotter. Read more about the background theory here. Email c2e2help@gmail.com for support.

Latest news

September, 2018: C2E2 ver 2.0 released for academic use. New features: Compositional modeling, model editing, new plotter, constant inputs.
May 15, 2017: C2E2 ver 1.0 released for academic use. New features: Thin variable, can work on Macs.

Version history. C2E2 implements the simulation-based verification approach described in the sequence of publications Duggirala et al. [2013, 2014, 2015]. From version 0.3 onward C2E2 (2016) uses an on-the-fly discrepancy computation algorithm described in Fan and Mitra [2015]. This eliminates the need for manual annotations (called discrepancy functions). New in version 2.0 (2018):

  • Compositional models
  • Thin input variables
  • Integrated hybrid model editor (.hyxml)
  • Model parsing error messaging
  • New general purpose reachtube plotter
  • Dropped support for Stateflow

New in version 1.0 (2016):

  • Full automation with on-the-fly discrepancy (no need for annotations)
  • Support for both CAPD or ODEINT simulations
  • Plotter for 2D sections of the reach sets computed.

Contributors. Lucas Brown, Parasara Sridhar Duggirala, Chuchu Fan, Zhenqi Huang, Suket Karnawat, Yangge Li, Yu Meng, Sayan Mitra, Matthew Potok, Bolun Qi, Vyom Thakkar, Mahesh Viswanathan, Le Wang.

Support. The research is in part supported by the National Science Foundation.

nsf4