  We present a tool for verification of hybrid systems expressed in the
sequential fragment of HCSP (Hybrid Communicating Sequential Processes). The
tool permits annotating HCSP programs with pre- and postconditions, invariants,
and proof rules for reasoning about ordinary differential equations.
Verification conditions are generated from the annotations following the rules
of hybrid Hoare logic. We designed labeling and highlighting mechanisms to
distinguish and visualize different verification conditions. The tool is
implemented in Python and has a web-based user interface. We evaluated the
effectiveness of the tool on translations of Simulink/Stateflow models and on
KeYmaera X benchmarks.
