Difference between revisions of "Maude Tools"

From The Maude System
Jump to: navigation, search
 
(13 intermediate revisions by 2 users not shown)
Line 1: Line 1:
 +
== Formal tools for Maude specifications ==
 +
* [https://nuitp.webs.upv.es/ NuITP] - An Inductive Theorem Prover 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://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/Maude-NPA/index.html 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 -->
 +
* [https://maude.cs.uiuc.edu/tools/createcinni createCINNI] - Automatic Generation of CINNI Instances for the Maude System
  
* [http://maude.cs.uiuc.edu/tools/itp/ Inductive Theorem Prover (ITP)]
+
==Extensions of Maude==
* [http://www.lcc.uma.es/~duran/MTT Maude Termination Tool]
+
* [https://olveczky.se/RealTimeMaude/ Real-Time Maude]
* [http://www.lcc.uma.es/~duran/ChC Coherence Checker]
+
* [https://maude.sip.ucm.es/strategies/index.html Maude Strategy Language]
* [http://heim.ifi.uio.no/~peterol/RealTimeMaude/ Real-Time Maude]
+
* [https://safe-tools.dsic.upv.es/acuos/ ACUOS]. Order-Sorted Modular ACU (Least General) Generalization System
* [http://maude.sip.ucm.es/strategies/index.html Maude Strategy Language]
+
 
* [http://maude.cs.uiuc.edu/tools/Maude-NPA/index.html Maude-NPA]
+
==Tools to assist in the development of Maude specifications==
* [http://maude.cs.uiuc.edu/tools/pvesta/index.html PVeStA]
+
* [https://maude.sip.ucm.es/debugging/ Declarative Debugger]
* [http://maude.sip.ucm.es/itp/ Inductive Theorem Prover (old version) with Web-ITP]
+
* [https://safe-tools.dsic.upv.es/anima/ The Anima tool] - Stepwise inspection of Maude computations
* [http://www.lcc.uma.es/~duran/CRC Church Rosser Checker]
+
* [https://safe-tools.dsic.upv.es/abets/ ABETS]. Assertion-based, Maude dynamic analyzer
* [http://maude.cs.illinois.edu/tools/scc/ Sufficient Completeness Checker]
+
* [https://safe-tools.dsic.upv.es/iJulienne/ iJulienne]. Backward Trace Slicer
* [http://maude.sip.ucm.es/~miguelpt/bibliography.html Predicate abstraction in Maude (see paper and tool from 2005)]
+
 
* [http://maude.sip.ucm.es/debugging/ Declarative Debugger]
+
==Tools for other formalisms and logics developed on Maude==
* [http://maude.cs.uiuc.edu/tools/rtp/ The Maude Resolution Theorem Prover (RTP)]
+
* [https://pl.csl.sri.com/ Pathway Logic Assistant] - Modeling of biological entities and processes
* [http://maude.cs.uiuc.edu/tools/tlr/ The Maude LTLR Model Checker]
+
* [https://fsl.cs.illinois.edu/index.php/Circ Circ] - An automated behavioral prover based on the circularity principle
* [http://maude.cs.uiuc.edu/tools/lmc/ The Maude LTL Logical Model Checker]
+
* [https://www.informatik.uni-hamburg.de/TGI/mitarbeiter/wimis/stehr/occ_eng.html OCC - An Open Calculus of Constructions]
* [http://maude.cs.illinois.edu/tools/eq-enrich/ Equality Enrichments for Order-Sorted Maude Theories]
+
* [https://maude.cs.uiuc.edu/maude1/casestudies/ccs CCS] and [http://maude.sip.ucm.es/~alberto/esf LOTOS]
* [[Maude Tools:Order-sorted Term Patterns|Order-sorted Term Patterns]]
+
 
* [http://safe-tools.dsic.upv.es/anima/ The Anima tool]
+
==Semantics and verification of programming languages==
 +
* [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, ...)==
 +
* [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==
 +
* [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:05, 20 March 2024

Formal tools for Maude specifications

Extensions of Maude

Tools to assist in the development of Maude specifications

Tools for other formalisms and logics developed on Maude

Semantics and verification of programming languages

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