====== HeKatE Verification and Analysis ======
HeaRT also provides a modularized verification framework, also known as HalVA (HeKatE Verification and Analysis).

===== Introduction =====

The framework uses the logical formalization of the [[XTT2]] model usling the [[ALSVfd]] logic.

It is based of previous work of Prof. Antoni Ligęza, and Dr. Grzegorz J. Nalepa.

Current implementation has been carried out by Agata Ligęza, MSc., with support of Szymon Bobek, MSc, and testing by Krzysztof Kaczor, MSc.

Verification and analysis module implements:
    *  simple debugging mechanism that allows tracking system's work,
    * export to LaTeX mechanism which provides functionality of exporting entire model to TEX file,
    * logical verification of models (several plugins are available, including completeness, determinism and redundancy checks), and
    * syntactic analysis of HMR files using a DCG grammar of HMR.
The verification plugins can be run from the interpreter or indirectly from HQEd using the communication protocol.

===== Documentation =====
See the general [[hekate:heart_overview#HeaRT Architecture]] and 
the [[hekate:heart_howto#Verifying Models]] howto.

===== Using it =====
HalVA is integrated with [[HeaRT]], so you need to [[hekate:heart#releases|download]] the engine.