MUTERM accepts various types of programs based on the use of rewrite rules and allows demonstrating the completion of computations performed by such programs. The tool works fully automatically on two levels. On the one hand it includes an expert who applies a series of techniques for the completion demonstration using a predefined strategy for this. In this mode the user can completely disregard the way the tool obtains the demonstration. On the other hand, it can be used to demonstrate termination using specific techniques. In this mode the user can specify various parameters to control the demonstration; this is useful for specialists and is also useful in teaching these techniques. In any case, the various options can be used without user intervention as default settings are set for immediate use. In both cases, the tool produces detailed reports listing the techniques applied to obtain the demonstration. MUTERM has participated with very good results in several international competitions along with tools of similar purpose.
See in the summary section
Program verification, safety analysis, provable security. Protocol crypto-analysis. Automated analysis, modeling, verification, synthesis, learning, debugging and optimization of complex systems and models