# Difference between revisions of "Maude Tools"

From The Maude System

Maudesystem (Talk | contribs) |
Maudesystem (Talk | contribs) |
||

Line 1: | Line 1: | ||

Formal tools for Maude specifications | Formal tools for Maude specifications | ||

− | * [https://code.google.com/p/maude-formal-environment/ The Maude Formal Environment] - Environment that integrates the Church-Rosser checker, the coherence checker, the termination tool | + | * [https://code.google.com/p/maude-formal-environment/ The Maude Formal Environment] - Environment that integrates the Church-Rosser checker, the coherence checker, and the termination tool |

* [http://maude.cs.uiuc.edu/tools/tlr/ The Maude LTLR Model Checker] | * [http://maude.cs.uiuc.edu/tools/tlr/ The Maude LTLR Model Checker] | ||

* [http://maude.cs.uiuc.edu/tools/lmc/ The Maude LTL Logical Model Checker] | * [http://maude.cs.uiuc.edu/tools/lmc/ The Maude LTL Logical Model Checker] |

## Revision as of 10:56, 13 May 2015

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
- PVeStA - A Parallel Statistical Model Checking and Quantitative Analysis Tool
- Inductive Theorem Prover (ITP)
- Sufficient Completeness Checker
- The Maude Resolution Theorem Prover (RTP)
- Maude-NPA - Maude-NRL Protocol Analyzer
- Equality Enrichments for Order-Sorted Maude Theories
- Order-sorted Term Patterns - A tool to discover term patterns
- createCINNI - Automatic Generation of CINNI Instances for the Maude System

Extensions of Maude

Tools to assist in the development of Maude specifications

- Declarative Debugger
- The Anima tool - Stepwise inspection of Maude computations

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

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

Other tools: