Compare Execute Check Engine (C2E2) is a tool for verifying bounded-time invariant properties of hybrid automata and Stateflow models. It supports models with nonlinear dynamics.

C2E2 implements the simulation-based verification approach described in the sequence of publications Duggirala et al. [2013, 2014, 2015]. The new C2E2 (v0.3 2016) uses an on-the-fly discrepancy computation algorithm described in Fan and Mitra [2015]. This eliminates the need for the user to provide annotations (called discrepancy functions).

C2E2 can take inputs in the form of Stateflow model (.mdl) or a hybrid automaton (.hyxml). It generates numerical simulations using CAPD or ODEINT, and it iteratively refines reach set over-approximations to prove invariants. It can also find counterexamples or bug traces. C2E2’s plotter can show 2D sections of the reach sets computed.

C2E2 is developed by the C2E2 development team at University of Illinois at Urbana-Champaign. Please email c2e2help@gmail.com for support.

The following individuals have contributed to development, testing and applications of C2E2: Parasara Sridhar Duggirala, Chuchu Fan, Zhenqi Huang, Sayan Mitra, Matthew Potok, Bolun Qi, Mahesh Viswanathan, Le Wang

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