Features

The following is an incomplete list of the provided features:

• An extended language
  • new set of types, namely 'Integer' and 'Reals'
  • new constructs to represent network of (hybrid-)automata (HyDi)
  • support for the AIGER format
• new advanced model checking algorithms
  • Full support for PSL model checking
  • Interpolation based invariant checking
    • CAV 2003 Mc Millan algorithm
    • Interpolation sequences algorithm
  • Guided reachability
    • Reachability analysis guided by a regular expression
  • Counter-Example Guided Abstraction Refinement (CEGAR)
    • Basic abstraction vial AllSMT
    • Advanced abstraction based on BDD and SMT
    • Refinement via Unsatisfiable Core and Interpolation
  • Infinite state model checking based on SMT techniques
    • Bounded Model Checking via SMT
    • Abstraction based
  • Compositional reasoning techniques
  • Model simplification and recoding techniques
    • Range Recoding
    • Free input propagation
• An extended set of functionalities
  • Requirements Analysis
    • Hybrid and Discrete
    • Property satisfiability
    • Property entailment
    • Unsatisfiable core extraction
    • Property realizability
  • Dependability Assessment
    • Fault tree analysis
    • FMEA analysis
    • FDIR verification
    • Diagnosability checks