The current folder contains examples to run invariant verification of hybrid systems.

README: this file.
bmc.cmd: run plain bounded model checking
shallow.cmd: run bmc using shallow synchronization semantic.
kind_abs.cmd: run kinduction with implicit predicate abstraction 
ic3.cmd: run ic3 with implicit predicate abstraction

Example to run INVAR verification:
../../hycomp -pre cpp -source ic3.cmd fisher_ring_2.hydi

NOTE:
- The script runs INVAR verification on ALL the properties contained
in the hydi model (you can specify the property to verify in the -n
  <prop_number> option of the verification command)

REFERENCES
Lei Bu, Alessandro Cimatti, Xuandong Li, Sergio Mover, Stefano Tonetta: Model Checking of Hybrid Systems Using Shallow Synchronization. FMOODS/FORTE 2010: 155-169