This is version 1.0 of hycomp

----------------------------------------------------------------------

HyComp is a model checker for asynchronous hybrid systems.
HyComp analyzes hybrid systems specified in the HyDI input language.

HyCOMP allow an user to model asynchronous hybrid systems with diffrent
dynamics (Linear Hybrid Automata, Linear Hybrid Systems, Polynomial
Hybrid Systems) and to analyze them with different verification
algorithms.

HyCOMP is based on the following tools:
  - the nuXmv model checker: https://nuxmv.fbk.eu/
  - the mathsat SMT solver: http://mathsat.fbk.eu/
  - the NuSMV model checker: http://nusmv.fbk.eu/

--------------------------------------------------------------------------------

HyCOMP is currently licensed in binary form, for non-commercial or
academic purposes. See LICENSE.txt for details.

Inquiries about other usages of hycomp should be addressed to
mover@fbk.eu, tonettas@fbk.eu, cimatti@fbk.eu

Visit https://es-static.fbk.eu/tools/hycomp/ for more detailed
information and download.

Other useful links:
* HyComp user mailing list: <still not available>
* Feature requests and bug reports: mover@fbk.eu
* Frequently asked questions: <still not available>

--------------------------------------------------------------------------------

HyCOMP Features:
  - Modelling of asynchronous hybrid systems (HyDI language) with the
    following dynamics:
    - Linear hybrid automata (LHA)
    - Linear hybrid systems (LHS)
    - Polynomial hybrid systems
  - Verification of invariant properties
  - Verification of LTL properties
  - Verification of scenario specifications

Upcoming features: in the next releases we will provide the following
features (See the references for more information): 
  - Abstraction techniques for LHS (relational abstraction)
  - Parameter synthesis algorithmsfor LHA

--------------------------------------------------------------------------------

People involved in the HyCOMP development:
  - Alessandro Cimatti: cimatti@fbk.eu
  - Alberto Griggio: griggio@fbk.eu
  - Sergio Mover: mover@fbk.eu
  - Stefano Tonetta: tonettas@fbk.eu


--------------------------------------------------------------------------------

The archive contains:
./README             -- this file
./LICENSE.txt        -- License File
./hycomp             -- The hycomp executable
./language.pdf       -- Tutorial on the HyDI language
./examples           -- A collection of examples/files used to run hycomp

--------------------------------------------------------------------------------

Disclaimer:
  - Documentation: the released version misses a manual on the usage
    of the commands.
    The example folders contains the stander sequences of commmands
    that should be invoked for all the basic task (e.g. invariant
    verification, ltl verification, ...).
    A manual will be provided in the following versions of the tool.
  - Support of dynamics in the released version: 

--------------------------------------------------------------------------------

References:

Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta: Verifying LTL Properties of Hybrid Systems with K-Liveness. CAV 2014: 424-440
Sergio Mover, Verification of Hybrid Systems using Satisfiability Modulo Theories, PhD Thesis (https://es-static.fbk.eu/people/mover/paper/mover_phd_thesis.pdf)
Alessandro Cimatti, Sergio Mover, Stefano Tonetta: Quantier-free encoding of invariants for Hybrid Systems, FMSD (DOI 10.1007/s10703-013-0202-8)
Alessandro Cimatti, Sergio Mover, Stefano Tonetta: SMT-based scenario verification for hybrid systems. Formal Methods in System Design 42(1): 46-66 (2013)
Alessandro Cimatti, Sergio Mover, Stefano Tonetta: A quantifier-free SMT encoding of non-linear hybrid automata. FMCAD 2012: 187-195
Alessandro Cimatti, Sergio Mover, Stefano Tonetta: Proving and explaining the unfeasibility of message sequence charts for hybrid systems. FMCAD 2011: 54-62
Alessandro Cimatti, Sergio Mover, Stefano Tonetta: Efficient Scenario Verification for Hybrid Automata. CAV 2011: 317-332
Alessandro Cimatti, Sergio Mover, Stefano Tonetta: HyDI: A Language for Symbolic Hybrid Systems with Discrete Interaction. EUROMICRO-SEAA 2011: 275-278
Lei Bu, Alessandro Cimatti, Xuandong Li, Sergio Mover, Stefano Tonetta: Model Checking of Hybrid Systems Using Shallow Synchronization. FMOODS/FORTE 2010: 155-169The current folder contains examples to run LTL verification of hybrid systems.

