lyg1597/c2e2-tool

The main verification tool

C2E2 Verification Tool

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. C2E2 (since ver 2.0, Sept 2018) supports compositional modeling, nonlinear dynamics, model editing, and has a powerful new plotter.

See home has a more information about background theory, examples, related publications, and results.

See C2E2 user's guide for detailed usage instructions.

Current version

Version 2.1 Summer 2020.

Features in current version

C2E2 implements the simulation-based verification approach described in the sequence of publications that appeared in Emsoft, CAV, TACAS, ATVA 2013-2018. Features in version 2.1 (2020):

• Open source release
• Command-line operations
• Compositional models
• GUI and text-based hybrid model editor (.hyxml)
• Improved model parsing error messaging
• Reachtube plotter
• Dropped support for Stateflow

Supported by

• National Science Foundation
• Air Force Office of Scientific Research