Difference between revisions of "Maude Tools"
From The Maude System
| (4 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
| − | Formal tools for Maude specifications | + | == Formal tools for Maude specifications == |
* [https://github.com/maude-team/MFE/wiki The Maude Formal Environment] - Environment that integrates the Church-Rosser checker, the coherence checker, and the termination tool | * [https://github.com/maude-team/MFE/wiki The Maude Formal Environment] - Environment that integrates the Church-Rosser checker, the coherence checker, and the termination tool | ||
| − | * [ | + | * [https://maude.cs.uiuc.edu/tools/tlr/ The Maude LTLR Model Checker] |
| − | * [ | + | * [https://maude.cs.uiuc.edu/tools/lmc/ The Maude LTL Logical Model Checker] |
| − | * [ | + | * [https://github.com/fadoss/umaudemc umaudemc] - A unified tool to check Maude specifications using external qualitative, probabilistic, and stochastical model checkers |
| − | * [ | + | * [https://maude.cs.uiuc.edu/tools/pvesta/index.html PVeStA] - A Parallel Statistical Model Checking and Quantitative Analysis Tool |
| − | * [ | + | * [https://sysma.imtlucca.it/tools/multivesta/ MultiVeStA] - A Distributed Statistical Model Checking for Discrete Event Simulators |
| − | * [ | + | * [https://maude.cs.uiuc.edu/tools/itp/ Inductive Theorem Prover (ITP)] |
| + | * [https://maude.cs.illinois.edu/tools/scc/ Sufficient Completeness Checker] | ||
<!-- * [http://maude.cs.uiuc.edu/tools/rtp/ The Maude Resolution Theorem Prover (RTP)] --> | <!-- * [http://maude.cs.uiuc.edu/tools/rtp/ The Maude Resolution Theorem Prover (RTP)] --> | ||
<!-- * [http://maude.cs.uiuc.edu/tools/Maude-NPA/index.html Maude-NPA] - Maude-NRL Protocol Analyzer --> | <!-- * [http://maude.cs.uiuc.edu/tools/Maude-NPA/index.html Maude-NPA] - Maude-NRL Protocol Analyzer --> | ||
* [[Maude Tools: Maude-NPA|Maude-NPA]] - Maude-NRL Protocol Analyzer | * [[Maude Tools: Maude-NPA|Maude-NPA]] - Maude-NRL Protocol Analyzer | ||
| − | * [ | + | * [https://maude.cs.illinois.edu/tools/eq-enrich/ Equality Enrichments for Order-Sorted Maude Theories] |
| − | * [[Maude Tools: Order-sorted Term Patterns|Order-sorted Term Patterns]] - A tool to discover term patterns | + | <!-- * [[Maude Tools: Order-sorted Term Patterns|Order-sorted Term Patterns]] - A tool to discover term patterns --> |
| − | * [ | + | * [https://maude.cs.uiuc.edu/tools/createcinni createCINNI] - Automatic Generation of CINNI Instances for the Maude System |
| − | Extensions of Maude | + | ==Extensions of Maude== |
| − | * [ | + | * [https://olveczky.se/RealTimeMaude/ Real-Time Maude] |
| − | * [ | + | * [https://maude.sip.ucm.es/strategies/index.html Maude Strategy Language] |
| − | * [ | + | * [https://safe-tools.dsic.upv.es/acuos/ ACUOS]. Order-Sorted Modular ACU (Least General) Generalization System |
| − | Tools to assist in the development of Maude specifications | + | ==Tools to assist in the development of Maude specifications== |
| − | * [ | + | * [https://maude.sip.ucm.es/debugging/ Declarative Debugger] |
| − | * [ | + | * [https://safe-tools.dsic.upv.es/anima/ The Anima tool] - Stepwise inspection of Maude computations |
| − | * [ | + | * [https://safe-tools.dsic.upv.es/abets/ ABETS]. Assertion-based, Maude dynamic analyzer |
| − | * [ | + | * [https://safe-tools.dsic.upv.es/iJulienne/ iJulienne]. Backward Trace Slicer |
| − | Tools for other formalisms and logics developed on Maude | + | ==Tools for other formalisms and logics developed on Maude== |
| − | * [ | + | * [https://pl.csl.sri.com/ Pathway Logic Assistant] - Modeling of biological entities and processes |
| − | * [ | + | * [https://fsl.cs.illinois.edu/index.php/Circ Circ] - An automated behavioral prover based on the circularity principle |
| − | * [ | + | * [https://www.informatik.uni-hamburg.de/TGI/mitarbeiter/wimis/stehr/occ_eng.html OCC - An Open Calculus of Constructions] |
| − | * [ | + | * [https://maude.cs.uiuc.edu/maude1/casestudies/ccs CCS] and [http://maude.sip.ucm.es/~alberto/esf LOTOS] |
| − | Semantics and verification of programming languages | + | ==Semantics and verification of programming languages== |
* [https://github.com/fcbr/mmt Maude MSOS tool] | * [https://github.com/fcbr/mmt Maude MSOS tool] | ||
| − | * [ | + | * [https://fsl.cs.illinois.edu/index.php/K_and_Matching_Logic The K framework and Matching logic] - Rewrite-based framework for the definition of formal operational semantics of programming languages |
| − | * [ | + | * [https://fsl.cs.illinois.edu/index.php/Rewriting_Logic_Semantics_of_Java JavaRL Rewriting specification of a Java semantics] - Java interpreter and formal analysis |
| − | * [ | + | * [https://fsl.cs.illinois.edu/index.php/JavaFAN JavaFAN] - Executable rewrite logic semantics of both Java and Java Bytecode using Maude |
| − | * [ | + | * [https://maude.cs.uiuc.edu/tools/javaitp Java+ITP] - A tool to prove Java properties |
| − | Web and Model-driven engineering (UML, OCL, MOF, model transformation, ...) | + | ==Web and Model-driven engineering (UML, OCL, MOF, model transformation, ...)== |
| − | * [ | + | * [https://maude.cs.illinois.edu/tools/synchaadl/ MR-SynchAADL] - Multirate Synchronous AADL and the MR-SynchAADL tool |
| − | * [ | + | * [https://moment.dsic.upv.es/ MOMENT] - A framework for model management |
| − | * [ | + | * [https://atenea.lcc.uma.es/e-motions e-Motions] - Visual definition of domain-specific modeling languages |
| − | * [ | + | * [https://maude.lcc.uma.es/mOdCL/ mOdCL] - UML/OCL specification, with static and dynamic evaluation of OCL expressions |
| − | * [ | + | * [https://zenon.dsic.upv.es:8080/webtlr/ Web-TLR]. A Model Checker for Web applications using LTLR |
| − | Other tools: | + | ==Other tools== |
| − | * [ | + | * [https://github.com/fadoss/maude-bindings Python's library] Language bindings to use Maude from other programming languages like Python |
| − | * [ | + | * [https://www.lcc.uma.es/~duran/MTT Maude Termination Tool] |
| − | * [ | + | * [https://www.lcc.uma.es/~duran/ChC Coherence Checker] |
| − | * [ | + | * [https://maude.sip.ucm.es/itp/ Inductive Theorem Prover (old version) with Web-ITP] |
| − | * [ | + | * [https://www.lcc.uma.es/~duran/CRC Church Rosser Checker] |
| − | * [ | + | * [https://maude.sip.ucm.es/mova ITP/OCL tool] |
| + | * [https://dl.acm.org/citation.cfm?id=1236626 MSR cryptoprotocol specification language (paper)] | ||
Latest revision as of 14:44, 29 March 2022
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)
