Henos is a tool that provides basic functionality for modeling and verification of reactive systems based on a mixture of automata/formula based specifications.