# Maude Tools

From The Maude System

## Contents

- 1 Formal tools for Maude specifications
- 2 Extensions of Maude
- 3 Tools to assist in the development of Maude specifications
- 4 Tools for other formalisms and logics developed on Maude
- 5 Semantics and verification of programming languages
- 6 Web and Model-driven engineering (UML, OCL, MOF, model transformation, ...)
- 7 Other tools

## Formal tools for Maude specifications

- The Maude Formal Environment - Environment that integrates the Church-Rosser checker, the coherence checker, and the termination tool
- The Maude LTLR Model Checker
- The Maude LTL Logical Model Checker
- umaudemc - A unified tool to check Maude specifications using external qualitative, probabilistic, and stochastical model checkers
- PVeStA - A Parallel Statistical Model Checking and Quantitative Analysis Tool
- MultiVeStA - A Distributed Statistical Model Checking for Discrete Event Simulators
- Inductive Theorem Prover (ITP)
- Sufficient Completeness Checker
- Maude-NPA - Maude-NRL Protocol Analyzer
- Equality Enrichments for Order-Sorted Maude Theories
- createCINNI - Automatic Generation of CINNI Instances for the Maude System

## Extensions of Maude

- Real-Time Maude
- Maude Strategy Language
- ACUOS. Order-Sorted Modular ACU (Least General) Generalization System

## Tools to assist in the development of Maude specifications

- Declarative Debugger
- The Anima tool - Stepwise inspection of Maude computations
- ABETS. Assertion-based, Maude dynamic analyzer
- iJulienne. Backward Trace Slicer

## Tools for other formalisms and logics developed on Maude

- Pathway Logic Assistant - Modeling of biological entities and processes
- Circ - An automated behavioral prover based on the circularity principle
- OCC - An Open Calculus of Constructions
- CCS and LOTOS

## Semantics and verification of programming languages

- Maude MSOS tool
- The K framework and Matching logic - Rewrite-based framework for the definition of formal operational semantics of programming languages
- JavaRL Rewriting specification of a Java semantics - Java interpreter and formal analysis
- JavaFAN - Executable rewrite logic semantics of both Java and Java Bytecode using Maude
- Java+ITP - A tool to prove Java properties

## Web and Model-driven engineering (UML, OCL, MOF, model transformation, ...)

- MR-SynchAADL - Multirate Synchronous AADL and the MR-SynchAADL tool
- MOMENT - A framework for model management
- e-Motions - Visual definition of domain-specific modeling languages
- mOdCL - UML/OCL specification, with static and dynamic evaluation of OCL expressions
- Web-TLR. A Model Checker for Web applications using LTLR

## Other tools

- Python's library Language bindings to use Maude from other programming languages like Python
- Maude Termination Tool
- Coherence Checker
- Inductive Theorem Prover (old version) with Web-ITP
- Church Rosser Checker
- ITP/OCL tool
- MSR cryptoprotocol specification language (paper)