This tool permits simplifying the analysis of Klaim and XKlaim systems. KlaiML allows to simulate Klaim and XKlaim programs and to generate their reachability graph. Moreover, using KlaiML, it is possible to verify whether a program satisfies a specified property.
The core of the system, which is implemented in OCaml, consists of two components: klaimlgraph (res. xklaimgraph) and klaimlprover (resp. xklaimprover). The first one permits analyzing the execution of Klaim programs and generating their reachability graphs. The second one, after loading a Klaim net and a formula , tests the satisfaction of the formula by the net. If the analyzed program has a finite reachability graph, klaimlprover exhibits the actual tree structure of the proof either for the formula or for its negation.
The results produced by klaimlgraph and klaimlprover are stored in XML format. These files can be visualized using the front-end components of the system: graphviewer and proofviewer. Finally, the tool also provides the component klamltop that permits using directly and interactively all modules oklaml.
Since KlaiML implementation is at a prototype level, we do not make the tool directly available on-line. However, everyone wants to obtain the software can send an e-mail.
