Welcome to the home page of the HyCOMP model checker for asynchronous hybrid systems.

HyCOMP is built on top of the nuXmv model checker https://es.fbk.eu/tools/nuXmv/ and of the Mathsat5 SMT solver http://mathsat.fbk.eu/

Main features:

  • HyDI language
  • Verification of invariant properties
  • Verification of LTL properties
  • Scenario verification
  • Parameter synthesis
  • Discretization of HyDI models to the nuXmv language (i.e. a symbolic transition systems)

Page last modified on October 23, 2014, at 07:40 PM