https://maude.cs.illinois.edu/w/api.php?action=feedcontributions&user=Malaga&feedformat=atomThe Maude System - User contributions [en]2024-03-29T07:09:11ZUser contributionsMediaWiki 1.23.1https://maude.cs.illinois.edu/w/index.php/Maude_download_and_installationMaude download and installation2024-03-21T20:20:07Z<p>Malaga: Fix in PDF link, Linux distributions</p>
<hr />
<div>Maude 3.4 runs on many Unix variants, including Linux. The installations is straightforward, there is one single executable file with no dependencies whatsoever. Nevertheless, some hints on how to use it and how to install it in Windows platforms can be found [[installation guidelines|here]].<br />
<br />
In this section, we assume a Linux configuration. Please, substitute your platform name for 'linux' in what follows if you download for another platform. <br />
In any case, please consider subscribing to the [[Maude Mailing Lists|Maude users mailing list]], as this is also the mechanism by which we will make announcements about the system.<br />
<br />
The Maude system download consists of the Maude binaries, and documentation and examples.<br />
<br />
The Linux64 and macOS versions of Maude 3.4 are available at [https://github.com/SRI-CSL/Maude/releases/tag/Maude3.4 its GitHub site]. <br />
Its sources are available from the same place. You can find instructions together with the sources. Some Linux distributions also offer Maude in their official repositories ([https://packages.debian.org/stable/maude Debian], [https://packages.ubuntu.com/maude Ubuntu], [https://archlinux.org/packages/extra/x86_64/maude/ ArchLinux], etc.), although their packages might not be up to date.<br />
<br />
To install from one of the above binaries, simply extract the downloaded zip file. This generates the folder with the following files in it:<br />
file.maude<br />
linear.maude<br />
machine-int.maude<br />
maude.[linux64|darwin64|arm64]<br />
metaInterpreter.maude<br />
model-checker.maude<br />
prelude.maude<br />
process.maude<br />
smt.maude<br />
socket.maude<br />
term-order.maude<br />
time.maude<br />
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude.linux64</tt>, <tt>maude.arm64</tt> or <tt>maude.darwin64</tt>.<br />
<br />
== Maude manual and primer ==<br />
<br />
The manual for Maude 3.4 is available in [[Media:Maude34manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The examples in the manual and in the book All About Maude is also available [[Media:Maude-3.4-manual-book-examples.zip|here]].<br />
<br />
== Main changes from Maude 3.3.1 to Maude 3.4 ==<br />
<br />
* Pseudo-random number generator objects<br />
* Initial equality operator<br />
* Meta-print to string operator and message pair<br />
* LaTeX support<br />
* =># search type<br />
* Various optimizations<br />
* Many bug fixes<br />
<br />
== Main changes from Maude 3.3 to 3.3.1 ==<br />
<br />
* Some overparsing has been added to provide more informative hints on user input. <br />
* Some bugs fixed.<br />
<br />
== Main changes from Maude 3.2.2 to 3.3 ==<br />
<br />
* Support for object-oriented features, including object-oriented modules and theories. Classes and messages can now be declared in object-oriented modules and theories, with multiple inheritance and their semantics specified using object-oriented statements that are automatically completed to simplify the specification of object-oriented systems. The handling of object-oriented features has been implemented as syntactic sugar, once entered object-oriented modules and theories are transformed into corresponding system modules and theories. <br />
* The module system has been extended to support the new object-oriented features. Elements in object-oriented modules can be renamed when imported, and object-oriented parameterized modules can be instantiated using views from object-oriented theories. All other modules operations have been correspondingly extended. <br />
* Modules can now be imported in a new generated-by mode. <br />
* Some new commands and flags have been added. <br />
* Constants can be declared as parameters in theories, and be parameterized in parameterized modules. <br />
* Full Maude is no longer distributed as part of Maude. It is still available from the [https://github.com/maude-team/full-maude Full Maude's github site].<br />
* Some over parsing has been added to better recover and to provide more informative hints on user input. <br />
* Some bugs fixed.<br />
<br />
== Main changes from Maude 3.2 to 3.2.2 ==<br />
<br />
* Improvement on the vu-narrow command<br />
<br />
== Main changes from Maude 3.1 to 3.2 ==<br />
<br />
* Support for filtered variant unification in vu-narrow command,<br />
* Several improvements in unification modulo several axioms,<br />
* Several improvements of the external Maude I/O objects,<br />
* A command flag for the depth of searching for A/AU unifiers, and<br />
* Some bugs fixed.<br />
<br />
== Change list from Maude 3.0 to 3.1 ==<br />
<br />
* Support for unification modulo associativity-identity,<br />
* Support for the generation of irredundant unifiers, <br />
* Support for the filtering of variant unifiers using variant subsumption,<br />
* Support for the generation of variant matchers, <br />
* An implementation of Unix processes as Maude external objects,<br />
* Several improvements in the presentation of results, <br />
* Several improvements in the handling of control-c, <br />
* Some bugs fixed, and<br />
* Some improvements in syntax error detection and recovering.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Maude_download_and_installationMaude download and installation2024-03-20T14:15:16Z<p>Malaga: /* Main changes from Maude 3.3.1 to Maude 3.4 = */</p>
<hr />
<div>Maude 3.4 runs on many Unix variants, including Linux. The installations is straightforward, there is one single executable file with no dependencies whatsoever. Nevertheless, some hints on how to use it and how to install it in Windows platforms can be found [[installation guidelines|here]].<br />
<br />
In this section, we assume a Linux configuration. Please, substitute your platform name for 'linux' in what follows if you download for another platform. <br />
In any case, please consider subscribing to the [[Maude Mailing Lists|Maude users mailing list]], as this is also the mechanism by which we will make announcements about the system.<br />
<br />
The Maude system download consists of the Maude binaries, and documentation and examples.<br />
<br />
The Linux64 and macOS versions of Maude 3.4 are available at [https://github.com/SRI-CSL/Maude/releases/tag/Maude3.4 its GitHub site]. <br />
Its sources are available from the same place. You can find instructions together with the sources. <br />
<br />
To install from one of the above binaries, simply extract the downloaded zip file. This generates the folder with the following files in it:<br />
file.maude<br />
linear.maude<br />
machine-int.maude<br />
maude.[linux64|darwin64|arm64]<br />
metaInterpreter.maude<br />
model-checker.maude<br />
prelude.maude<br />
process.maude<br />
smt.maude<br />
socket.maude<br />
term-order.maude<br />
time.maude<br />
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude.linux64</tt>, <tt>maude.arm64</tt> or <tt>maude.darwin64</tt>.<br />
<br />
== Maude manual and primer ==<br />
<br />
The manual for Maude 3.4 is available in [[Media:Maude-3.4-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The examples in the manual and in the book All About Maude is also available [[Media:Maude-3.4-manual-book-examples.zip|here]].<br />
<br />
== Main changes from Maude 3.3.1 to Maude 3.4 ==<br />
<br />
* Pseudo-random number generator objects<br />
* Initial equality operator<br />
* Meta-print to string operator and message pair<br />
* LaTeX support<br />
* =># search type<br />
* Various optimizations<br />
* Many bug fixes<br />
<br />
== Main changes from Maude 3.3 to 3.3.1 ==<br />
<br />
* Some overparsing has been added to provide more informative hints on user input. <br />
* Some bugs fixed.<br />
<br />
== Main changes from Maude 3.2.2 to 3.3 ==<br />
<br />
* Support for object-oriented features, including object-oriented modules and theories. Classes and messages can now be declared in object-oriented modules and theories, with multiple inheritance and their semantics specified using object-oriented statements that are automatically completed to simplify the specification of object-oriented systems. The handling of object-oriented features has been implemented as syntactic sugar, once entered object-oriented modules and theories are transformed into corresponding system modules and theories. <br />
* The module system has been extended to support the new object-oriented features. Elements in object-oriented modules can be renamed when imported, and object-oriented parameterized modules can be instantiated using views from object-oriented theories. All other modules operations have been correspondingly extended. <br />
* Modules can now be imported in a new generated-by mode. <br />
* Some new commands and flags have been added. <br />
* Constants can be declared as parameters in theories, and be parameterized in parameterized modules. <br />
* Full Maude is no longer distributed as part of Maude. It is still available from the [https://github.com/maude-team/full-maude Full Maude's github site].<br />
* Some over parsing has been added to better recover and to provide more informative hints on user input. <br />
* Some bugs fixed.<br />
<br />
== Main changes from Maude 3.2 to 3.2.2 ==<br />
<br />
* Improvement on the vu-narrow command<br />
<br />
== Main changes from Maude 3.1 to 3.2 ==<br />
<br />
* Support for filtered variant unification in vu-narrow command,<br />
* Several improvements in unification modulo several axioms,<br />
* Several improvements of the external Maude I/O objects,<br />
* A command flag for the depth of searching for A/AU unifiers, and<br />
* Some bugs fixed.<br />
<br />
== Change list from Maude 3.0 to 3.1 ==<br />
<br />
* Support for unification modulo associativity-identity,<br />
* Support for the generation of irredundant unifiers, <br />
* Support for the filtering of variant unifiers using variant subsumption,<br />
* Support for the generation of variant matchers, <br />
* An implementation of Unix processes as Maude external objects,<br />
* Several improvements in the presentation of results, <br />
* Several improvements in the handling of control-c, <br />
* Some bugs fixed, and<br />
* Some improvements in syntax error detection and recovering.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Maude_download_and_installationMaude download and installation2024-03-20T14:15:00Z<p>Malaga: </p>
<hr />
<div>Maude 3.4 runs on many Unix variants, including Linux. The installations is straightforward, there is one single executable file with no dependencies whatsoever. Nevertheless, some hints on how to use it and how to install it in Windows platforms can be found [[installation guidelines|here]].<br />
<br />
In this section, we assume a Linux configuration. Please, substitute your platform name for 'linux' in what follows if you download for another platform. <br />
In any case, please consider subscribing to the [[Maude Mailing Lists|Maude users mailing list]], as this is also the mechanism by which we will make announcements about the system.<br />
<br />
The Maude system download consists of the Maude binaries, and documentation and examples.<br />
<br />
The Linux64 and macOS versions of Maude 3.4 are available at [https://github.com/SRI-CSL/Maude/releases/tag/Maude3.4 its GitHub site]. <br />
Its sources are available from the same place. You can find instructions together with the sources. <br />
<br />
To install from one of the above binaries, simply extract the downloaded zip file. This generates the folder with the following files in it:<br />
file.maude<br />
linear.maude<br />
machine-int.maude<br />
maude.[linux64|darwin64|arm64]<br />
metaInterpreter.maude<br />
model-checker.maude<br />
prelude.maude<br />
process.maude<br />
smt.maude<br />
socket.maude<br />
term-order.maude<br />
time.maude<br />
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude.linux64</tt>, <tt>maude.arm64</tt> or <tt>maude.darwin64</tt>.<br />
<br />
== Maude manual and primer ==<br />
<br />
The manual for Maude 3.4 is available in [[Media:Maude-3.4-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The examples in the manual and in the book All About Maude is also available [[Media:Maude-3.4-manual-book-examples.zip|here]].<br />
<br />
== Main changes from Maude 3.3.1 to Maude 3.4 ===<br />
<br />
* Pseudo-random number generator objects<br />
* Initial equality operator<br />
* Meta-print to string operator and message pair<br />
* LaTeX support<br />
* =># search type<br />
* Various optimizations<br />
* Many bug fixes<br />
<br />
== Main changes from Maude 3.3 to 3.3.1 ==<br />
<br />
* Some overparsing has been added to provide more informative hints on user input. <br />
* Some bugs fixed.<br />
<br />
== Main changes from Maude 3.2.2 to 3.3 ==<br />
<br />
* Support for object-oriented features, including object-oriented modules and theories. Classes and messages can now be declared in object-oriented modules and theories, with multiple inheritance and their semantics specified using object-oriented statements that are automatically completed to simplify the specification of object-oriented systems. The handling of object-oriented features has been implemented as syntactic sugar, once entered object-oriented modules and theories are transformed into corresponding system modules and theories. <br />
* The module system has been extended to support the new object-oriented features. Elements in object-oriented modules can be renamed when imported, and object-oriented parameterized modules can be instantiated using views from object-oriented theories. All other modules operations have been correspondingly extended. <br />
* Modules can now be imported in a new generated-by mode. <br />
* Some new commands and flags have been added. <br />
* Constants can be declared as parameters in theories, and be parameterized in parameterized modules. <br />
* Full Maude is no longer distributed as part of Maude. It is still available from the [https://github.com/maude-team/full-maude Full Maude's github site].<br />
* Some over parsing has been added to better recover and to provide more informative hints on user input. <br />
* Some bugs fixed.<br />
<br />
== Main changes from Maude 3.2 to 3.2.2 ==<br />
<br />
* Improvement on the vu-narrow command<br />
<br />
== Main changes from Maude 3.1 to 3.2 ==<br />
<br />
* Support for filtered variant unification in vu-narrow command,<br />
* Several improvements in unification modulo several axioms,<br />
* Several improvements of the external Maude I/O objects,<br />
* A command flag for the depth of searching for A/AU unifiers, and<br />
* Some bugs fixed.<br />
<br />
== Change list from Maude 3.0 to 3.1 ==<br />
<br />
* Support for unification modulo associativity-identity,<br />
* Support for the generation of irredundant unifiers, <br />
* Support for the filtering of variant unifiers using variant subsumption,<br />
* Support for the generation of variant matchers, <br />
* An implementation of Unix processes as Maude external objects,<br />
* Several improvements in the presentation of results, <br />
* Several improvements in the handling of control-c, <br />
* Some bugs fixed, and<br />
* Some improvements in syntax error detection and recovering.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Some_Papers_on_Maude_and_on_Rewriting_LogicSome Papers on Maude and on Rewriting Logic2024-03-20T14:08:43Z<p>Malaga: </p>
<hr />
<div>A friendly introduction to the latest advances in the symbolic features of Maude will appear in Proc. LOPSTER 2020: [[Media:maude-tapas.pdf|Symbolic Computation in Maude: Some Tapas]].<br />
<br />
In-depth presentations of Maude, and on how to use its most common features, are available in the following books: <br />
<br />
* M. Clavel et al.: [https://doi.org/10.1007/978-3-540-71999-1 All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic]. LNCS 4350, Springer (2007)<br />
<br />
* P.C. Ölveczky: [https://doi.org/10.1007/978-1-4471-6687-0 Designing Reliable Distributed Systems - A Formal Methods Approach Based on Executable Modeling in Maude]. Springer (2017)<br />
<br />
Several bibliographies and surveys on rewriting logic and Maude have been published:<br />
<br />
* M. Clavel et al.: [https://doi.org/10.1007/978-3-319-23165-5_11 Two Decades of Maude]. Logic, Rewriting, and Concurrency: 232-254 (2015). A pre-print is available [[Media:Two-Decades-of-Maude.pdf|here]].<br />
<br />
* J. Meseguer: [https://doi.org/10.1016/j.jlap.2012.06.003 Twenty years of rewriting logic]. J. Log. Algebraic Methods Program. 81(7-8): 721-781 (2012). A pre-print is available [[Media:20-years.pdf|here]].<br />
<br />
* N. Martí-Oliet, M. Palomino, and A. Verdejo: [https://www.sciencedirect.com/science/article/pii/S1567832612000562?via%3Dihub Rewriting logic bibliography by topic: 1990–2011]. J. Log. Algebraic Methods Program. 81: 782-815 (2012)<br />
<br />
* N. Martí-Oliet and J. Meseguer: [https://www.sciencedirect.com/science/article/pii/S0304397501003577 Rewriting logic: roadmap and bibliography]. Theor. Comput. Sci. 285(2): 121-154 (2002). A pre-print is available [[Media:MMroadmap_2001.pdf|here]].<br />
<br />
The following papers may serve as a selection of such huge body of work:<br />
<br />
* S. Eker et al.: [https://doi.org/10.1016/j.jlamp.2023.100887 The Maude strategy language]. J. Log. Algebraic Methods Program. 134: 100887 (2023)<br />
<br />
* S. Liu et al.: [https://doi.org/10.1145/3563299 Bridging the semantic gap between qualitative and quantitative models of distributed systems]. Proc. ACM Program. Lang. 6 (OOPSLA2): 315-344 (2022)<br />
<br />
* F. Durán et al.: [https://doi.org/10.1016/j.jlamp.2019.100497 Programming and symbolic computation in Maude]. J. Log. Algebraic Methods Program. 110 (2020). A pre-print is available [[Media:maude-jlamp.pdf|here]].<br />
<br />
* J. Meseguer: [https://doi.org/10.1016/j.jlamp.2019.100483 Generalized rewrite theories, coherence completion, and symbolic methods]. J. Log. Algebraic Methods Program. 110 (2020). A pre-print is available [[Media:BMgrt_2003.pdf|here]].<br />
<br />
* F. Durán, J. Meseguer, and C. Rocha: [https://doi.org/10.1016/j.jlamp.2019.100513 Ground confluence of order-sorted conditional specifications modulo axioms]. J. Log. Algebraic Methods Program. 111: 100513 (2020). A pre-print is available [[Media:Durán.Mesegue.Rocha.Ground Confluence of Order-sorted Conditional Specifications Modulo Axioms.TR.pdf|here]].<br />
<br />
* C. Rocha, J. Meseguer, C. Muñoz: [https://doi.org/10.1016/j.jlamp.2016.10.001 Rewriting modulo SMT and open system analysis]. J. Log. Algebraic Methods Program. 86(1): 269-297 (2017)<br />
<br />
* S. Escobar, R. Sasse, J. Meseguer: [https://doi.org/10.1016/j.jlap.2012.01.002 Folding variant narrowing and optimal variant termination]. J. Log. Algebraic Methods Program. 81(7-8): 898-928 (2012)<br />
<br />
* F. Durán and J. Meseguer: [https://doi.org/10.1016/j.jlap.2011.12.004 On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories]. J. Log. Algebraic Methods Program. 81(7-8): 816-850 (2012). A pre-print is available [[Media:CRChC.pdf|here]].<br />
<br />
* J. Meseguer, M. Palomino, and N. Martí-Oliet: [https://doi.org/10.1016/j.jlap.2009.07.003 Algebraic simulations]. J. Log. Algebraic Methods Program. 79(2): 103-143 (2010). A pre-print is available [[Media:MartiOlietEtAl03-journal.pdf|here]].<br />
<br />
* J. Meseguer, M. Palomino, and N. Martí-Oliet: [https://doi.org/10.1016/j.tcs.2008.04.040 Equational abstractions]. Theor. Comput. Sci. 403(2-3): 239-264 (2008). A pre-print is available [[Media:MPMea_2003.pdf|here]].<br />
<br />
* M. Clavel, J. Meseguer, and M. Palomino: [https://doi.org/10.1016/j.tcs.2006.12.009 Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic]. Theor. Comput. Sci. 373(1-2): 70-91 (2007)<br />
<br />
* P.C. Ölveczky and J. Meseguer: [https://doi.org/10.1007/s10990-007-9001-5 Semantics and pragmatics of Real-Time Maude]. High. Order Symb. Comput. 20(1-2): 161-196 (2007)<br />
<br />
* F. Durán and J. Meseguer: [https://doi.org/10.1016/j.scico.2006.07.002 Maude's module algebra]. Sci. Comput. Program. 66(2): 125-153 (2007)<br />
<br />
* R. Bruni and J. Meseguer: [https://doi.org/10.1016/j.tcs.2006.04.012 Semantic foundations for generalized rewrite theories]. Theor. Comput. Sci. 360(1-3): 386-414 (2006)<br />
<br />
* M. Clavel et al.: [https://doi.org/10.1016/S0304-3975(01)00359-0 Maude: specification and programming in rewriting logic]. Theor. Comput. Sci. 285(2): 187-243 (2002). A pre-print is available [[Media:CDELMMQspecprog_2001.pdf|here]].<br />
<br />
* J. Meseguer: [https://doi.org/10.1007/3-540-64299-4_26 Membership algebra as a logical framework for equational specification]. WADT: 18-61 (1997)<br />
<br />
* N. Martí-Oliet and J. Meseguer: [https://doi.org/10.1016/S1571-0661(04)00040-4 Rewriting logic as a logical and semantic framework]. WRLA: 190-225 (1996)<br />
<br />
* J. Meseguer: [https://www.sciencedirect.com/science/article/pii/030439759290182F Conditional rewriting logic as a unified model of concurrency]. Theor. Comput. Sci. 96(1): 73-155 (1996)<br />
<br />
Some Additional Papers on Maude and on Rewriting Logic are available [http://maude.cs.illinois.edu/papers/ here].</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Maude_ToolsMaude Tools2024-03-20T14:05:02Z<p>Malaga: </p>
<hr />
<div>== Formal tools for Maude specifications ==<br />
* [https://nuitp.webs.upv.es/ NuITP] - An Inductive Theorem Prover for Maude Specifications]<br />
* [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<br />
* [https://maude.cs.uiuc.edu/tools/tlr/ The Maude LTLR Model Checker]<br />
* [https://maude.cs.uiuc.edu/tools/lmc/ The Maude LTL Logical Model Checker]<br />
* [https://github.com/fadoss/umaudemc umaudemc] - A unified tool to check Maude specifications using external qualitative, probabilistic, and stochastical model checkers<br />
* [https://maude.cs.uiuc.edu/tools/pvesta/index.html PVeStA] - A Parallel Statistical Model Checking and Quantitative Analysis Tool<br />
* [https://sysma.imtlucca.it/tools/multivesta/ MultiVeStA] - A Distributed Statistical Model Checking for Discrete Event Simulators<br />
* [https://maude.cs.uiuc.edu/tools/itp/ Inductive Theorem Prover (ITP)]<br />
* [https://maude.cs.illinois.edu/tools/scc/ Sufficient Completeness Checker]<br />
<!-- * [http://maude.cs.uiuc.edu/tools/rtp/ The Maude Resolution Theorem Prover (RTP)] --><br />
<!-- * [http://maude.cs.uiuc.edu/tools/Maude-NPA/index.html Maude-NPA] - Maude-NRL Protocol Analyzer --><br />
* [[Maude Tools: Maude-NPA|Maude-NPA]] - Maude-NRL Protocol Analyzer<br />
* [https://maude.cs.illinois.edu/tools/eq-enrich/ Equality Enrichments for Order-Sorted Maude Theories]<br />
<!-- * [[Maude Tools: Order-sorted Term Patterns|Order-sorted Term Patterns]] - A tool to discover term patterns --><br />
* [https://maude.cs.uiuc.edu/tools/createcinni createCINNI] - Automatic Generation of CINNI Instances for the Maude System<br />
<br />
==Extensions of Maude==<br />
* [https://olveczky.se/RealTimeMaude/ Real-Time Maude]<br />
* [https://maude.sip.ucm.es/strategies/index.html Maude Strategy Language]<br />
* [https://safe-tools.dsic.upv.es/acuos/ ACUOS]. Order-Sorted Modular ACU (Least General) Generalization System<br />
<br />
==Tools to assist in the development of Maude specifications==<br />
* [https://maude.sip.ucm.es/debugging/ Declarative Debugger]<br />
* [https://safe-tools.dsic.upv.es/anima/ The Anima tool] - Stepwise inspection of Maude computations<br />
* [https://safe-tools.dsic.upv.es/abets/ ABETS]. Assertion-based, Maude dynamic analyzer<br />
* [https://safe-tools.dsic.upv.es/iJulienne/ iJulienne]. Backward Trace Slicer<br />
<br />
==Tools for other formalisms and logics developed on Maude==<br />
* [https://pl.csl.sri.com/ Pathway Logic Assistant] - Modeling of biological entities and processes<br />
* [https://fsl.cs.illinois.edu/index.php/Circ Circ] - An automated behavioral prover based on the circularity principle<br />
* [https://www.informatik.uni-hamburg.de/TGI/mitarbeiter/wimis/stehr/occ_eng.html OCC - An Open Calculus of Constructions]<br />
* [https://maude.cs.uiuc.edu/maude1/casestudies/ccs CCS] and [http://maude.sip.ucm.es/~alberto/esf LOTOS]<br />
<br />
==Semantics and verification of programming languages==<br />
* [https://github.com/fcbr/mmt Maude MSOS tool]<br />
* [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<br />
* [https://fsl.cs.illinois.edu/index.php/Rewriting_Logic_Semantics_of_Java JavaRL Rewriting specification of a Java semantics] - Java interpreter and formal analysis<br />
* [https://fsl.cs.illinois.edu/index.php/JavaFAN JavaFAN] - Executable rewrite logic semantics of both Java and Java Bytecode using Maude<br />
* [https://maude.cs.uiuc.edu/tools/javaitp Java+ITP] - A tool to prove Java properties<br />
<br />
==Web and Model-driven engineering (UML, OCL, MOF, model transformation, ...)==<br />
* [https://maude.cs.illinois.edu/tools/synchaadl/ MR-SynchAADL] - Multirate Synchronous AADL and the MR-SynchAADL tool<br />
* [https://moment.dsic.upv.es/ MOMENT] - A framework for model management<br />
* [https://atenea.lcc.uma.es/e-motions e-Motions] - Visual definition of domain-specific modeling languages<br />
* [https://maude.lcc.uma.es/mOdCL/ mOdCL] - UML/OCL specification, with static and dynamic evaluation of OCL expressions<br />
* [https://zenon.dsic.upv.es:8080/webtlr/ Web-TLR]. A Model Checker for Web applications using LTLR<br />
<br />
==Other tools==<br />
* [https://github.com/fadoss/maude-bindings Python's library] Language bindings to use Maude from other programming languages like Python<br />
* [https://www.lcc.uma.es/~duran/MTT Maude Termination Tool]<br />
* [https://www.lcc.uma.es/~duran/ChC Coherence Checker]<br />
* [https://maude.sip.ucm.es/itp/ Inductive Theorem Prover (old version) with Web-ITP]<br />
* [https://www.lcc.uma.es/~duran/CRC Church Rosser Checker]<br />
* [https://maude.sip.ucm.es/mova ITP/OCL tool]<br />
* [https://dl.acm.org/citation.cfm?id=1236626 MSR cryptoprotocol specification language (paper)]</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2024-03-20T14:03:10Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: full C ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), Java ([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), JVM ([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), [https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] ([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), Verilog ([https://ieeexplore.ieee.org/document/5558634 MKMR10]), E-LOTOS ([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], [https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), UML ([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], [https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), MOF ([https://doi.org/10.1007/s00165-009-0140-9 BM10]), ODP ([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], [https://doi.org/10.1016/j.csi.2004.10.008 DRV05], [https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), AADL ([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], [https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), Ptolemy ([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), BPMN ([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], [https://doi.org/10.1016/j.scico.2018.08.007 DRS18], [https://doi.org/10.1007/978-3-031-12441-9_6 DMC23], [https://doi.org/10.1016/j.jlamp.2023.100928 DPR24]), DSMLs ([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], [https://doi.org/10.1177/0037549709341635 RDV09], [https://doi.org/10.5381/jot.2022.21.4.a2 D23]), Multi-Level Modelling Languages ([https://doi.org/10.1016/j.jlamp.2022.100831 RMDRW23], [https://doi.org/10.1007/s10270-021-00947-1 RDK23]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and design and verification of the secure-by-construction Illinois’s IBOS browser ([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], [https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Networks: AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); DDoS-Intruder models; and DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool]. Secure bandwidth reservation in path-aware Internet architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), end-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]). SCION’s bandwidth allocation protocol ([https://link.springer.com/book/10.1007/978-3-031-05288-0 CLBHHMP22]).<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2024-03-20T14:02:14Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: full C ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), Java ([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), JVM ([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), [https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] ([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), Verilog ([https://ieeexplore.ieee.org/document/5558634 MKMR10]), E-LOTOS ([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], [https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), UML ([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], [https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), MOF ([https://doi.org/10.1007/s00165-009-0140-9 BM10]), ODP ([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], [https://doi.org/10.1016/j.csi.2004.10.008 DRV05], [https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), AADL ([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], [https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), Ptolemy ([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), BPMN ([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], [https://doi.org/10.1016/j.scico.2018.08.007 DRS18], [https://doi.org/10.1007/978-3-031-12441-9_6 DMC23], [https://doi.org/10.1016/j.jlamp.2023.100928 DPR24]), DSMLs ([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], [https://doi.org/10.1177/0037549709341635 RDV09], [https://doi.org/10.5381/jot.2022.21.4.a2 D23]), Multi-Level Modelling Languages ([https://doi.org/10.1016/j.jlamp.2022.100831 RMDRW23], [https://doi.org/10.1007/s10270-021-00947-1 RDK23]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and design and verification of the secure-by-construction Illinois’s IBOS browser ([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], <br />
[https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Networks: AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); DDoS-Intruder models; and DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool]. Secure bandwidth reservation in path-aware Internet architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), end-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]). SCION’s bandwidth allocation protocol ([https://link.springer.com/book/10.1007/978-3-031-05288-0 CLBHHMP22]).<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2024-03-20T14:01:20Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: full C ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), Java ([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), JVM ([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), [https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] ([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), Verilog ([https://ieeexplore.ieee.org/document/5558634 MKMR10]), E-LOTOS ([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], [https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), UML ([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], [https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), MOF ([https://doi.org/10.1007/s00165-009-0140-9 BM10]), ODP ([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], [https://doi.org/10.1016/j.csi.2004.10.008 DRV05], [https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), AADL ([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], [https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), Ptolemy ([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), BPMN ([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], [https://doi.org/10.1016/j.scico.2018.08.007 DRS18], [https://doi.org/10.1007/978-3-031-12441-9_6 DMC23], [https://doi.org/10.1016/j.jlamp.2023.100928 DPR24]), DSMLs ([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], [https://doi.org/10.1177/0037549709341635 RDV09], [https://doi.org/10.5381/jot.2022.21.4.a2 D23]), Multi-Level Modelling Languages ([https://doi.org/10.1016/j.jlamp.2022.100831 RMDRW23],<br />
[https://doi.org/10.1007/s10270-021-00947-1 RDK23]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and design and verification of the secure-by-construction Illinois’s IBOS browser ([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], <br />
[https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Networks: AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); DDoS-Intruder models; and <br />
DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): <br />
ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), <br />
Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), <br />
VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool]. <br />
Secure bandwidth reservation in path-aware Internet architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), <br />
end-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]).<br />
SCION’s bandwidth allocation protocol ([https://link.springer.com/book/10.1007/978-3-031-05288-0 CLBHHMP22]).<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2024-03-20T14:00:30Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: full C ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), Java <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), <br />
JVM ([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), <br />
[https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] <br />
([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), <br />
Verilog ([https://ieeexplore.ieee.org/document/5558634 MKMR10]), <br />
E-LOTOS ([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], <br />
[https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), <br />
UML ([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], <br />
[https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), <br />
MOF ([https://doi.org/10.1007/s00165-009-0140-9 BM10]), <br />
ODP ([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], <br />
[https://doi.org/10.1016/j.csi.2004.10.008 DRV05], <br />
[https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), <br />
AADL ([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], <br />
[https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), <br />
Ptolemy ([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), <br />
BPMN ([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], <br />
[https://doi.org/10.1016/j.scico.2018.08.007 DRS18], <br />
[https://doi.org/10.1007/978-3-031-12441-9_6 DMC23], <br />
[https://doi.org/10.1016/j.jlamp.2023.100928 DPR24]), <br />
DSMLs ([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], <br />
[https://doi.org/10.1177/0037549709341635 RDV09],<br />
[https://doi.org/10.5381/jot.2022.21.4.a2 D23]),<br />
Multi-Level Modelling Languages ([https://doi.org/10.1016/j.jlamp.2022.100831 RMDRW23],<br />
[https://doi.org/10.1007/s10270-021-00947-1 RDK23]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and design and verification of the secure-by-construction Illinois’s IBOS browser ([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], <br />
[https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Networks: AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); DDoS-Intruder models; and <br />
DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): <br />
ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), <br />
Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), <br />
VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool]. <br />
Secure bandwidth reservation in path-aware Internet architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), <br />
end-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]).<br />
SCION’s bandwidth allocation protocol ([https://link.springer.com/book/10.1007/978-3-031-05288-0 CLBHHMP22]).<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2024-03-20T13:59:46Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: full C ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), Java <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), <br />
JVM <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), <br />
[https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] <br />
([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), <br />
Verilog <br />
([https://ieeexplore.ieee.org/document/5558634 MKMR10]), <br />
E-LOTOS <br />
([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], <br />
[https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), <br />
UML <br />
([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], <br />
[https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), <br />
MOF <br />
([https://doi.org/10.1007/s00165-009-0140-9 BM10]), <br />
ODP <br />
([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], <br />
[https://doi.org/10.1016/j.csi.2004.10.008 DRV05], <br />
[https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), <br />
AADL <br />
([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], <br />
[https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), <br />
Ptolemy <br />
([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), <br />
BPMN <br />
([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], <br />
[https://doi.org/10.1016/j.scico.2018.08.007 DRS18], <br />
[https://doi.org/10.1007/978-3-031-12441-9_6 DMC23], <br />
[https://doi.org/10.1016/j.jlamp.2023.100928 DPR24]), <br />
DSMLs <br />
([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], <br />
[https://doi.org/10.1177/0037549709341635 RDV09],<br />
[https://doi.org/10.5381/jot.2022.21.4.a2 D23]),<br />
Multi-Level Modelling Languages <br />
([https://doi.org/10.1016/j.jlamp.2022.100831 RMDRW23],<br />
[https://doi.org/10.1007/s10270-021-00947-1 RDK23]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and design and verification of the secure-by-construction Illinois’s IBOS browser ([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], <br />
[https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Networks: AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), <br />
BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); <br />
DDoS-Intruder models; and <br />
DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): <br />
ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), <br />
Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), <br />
VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool]. <br />
Secure bandwidth reservation in path-aware Internet architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), <br />
end-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]).<br />
SCION’s bandwidth allocation protocol ([https://link.springer.com/book/10.1007/978-3-031-05288-0 CLBHHMP22]).<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2024-03-20T13:59:17Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: full C ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), <br />
Java <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), <br />
JVM <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), <br />
[https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] <br />
([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), <br />
Verilog <br />
([https://ieeexplore.ieee.org/document/5558634 MKMR10]), <br />
E-LOTOS <br />
([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], <br />
[https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), <br />
UML <br />
([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], <br />
[https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), <br />
MOF <br />
([https://doi.org/10.1007/s00165-009-0140-9 BM10]), <br />
ODP <br />
([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], <br />
[https://doi.org/10.1016/j.csi.2004.10.008 DRV05], <br />
[https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), <br />
AADL <br />
([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], <br />
[https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), <br />
Ptolemy <br />
([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), <br />
BPMN <br />
([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], <br />
[https://doi.org/10.1016/j.scico.2018.08.007 DRS18], <br />
[https://doi.org/10.1007/978-3-031-12441-9_6 DMC23], <br />
[https://doi.org/10.1016/j.jlamp.2023.100928 DPR24]), <br />
DSMLs <br />
([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], <br />
[https://doi.org/10.1177/0037549709341635 RDV09],<br />
[https://doi.org/10.5381/jot.2022.21.4.a2 D23]),<br />
Multi-Level Modelling Languages <br />
([https://doi.org/10.1016/j.jlamp.2022.100831 RMDRW23],<br />
[https://doi.org/10.1007/s10270-021-00947-1 RDK23]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and <br />
design and verification of the secure-by-construction Illinois’s IBOS browser ([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], <br />
[https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Networks: AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), <br />
MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), <br />
BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); <br />
DDoS-Intruder models; and <br />
DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): <br />
ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), <br />
Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), <br />
VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool]. <br />
Secure bandwidth reservation in path-aware Internet architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), <br />
end-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]).<br />
SCION’s bandwidth allocation protocol ([https://link.springer.com/book/10.1007/978-3-031-05288-0 CLBHHMP22]).<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2024-03-20T13:58:52Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: full C ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), <br />
Java <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), <br />
JVM <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), <br />
[https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] <br />
([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), <br />
Verilog <br />
([https://ieeexplore.ieee.org/document/5558634 MKMR10]), <br />
E-LOTOS <br />
([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], <br />
[https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), <br />
UML <br />
([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], <br />
[https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), <br />
MOF <br />
([https://doi.org/10.1007/s00165-009-0140-9 BM10]), <br />
ODP <br />
([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], <br />
[https://doi.org/10.1016/j.csi.2004.10.008 DRV05], <br />
[https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), <br />
AADL <br />
([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], <br />
[https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), <br />
Ptolemy <br />
([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), <br />
BPMN <br />
([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], <br />
[https://doi.org/10.1016/j.scico.2018.08.007 DRS18], <br />
[https://doi.org/10.1007/978-3-031-12441-9_6 DMC23], <br />
[https://doi.org/10.1016/j.jlamp.2023.100928 DPR24]), <br />
DSMLs <br />
([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], <br />
[https://doi.org/10.1177/0037549709341635 RDV09],<br />
[https://doi.org/10.5381/jot.2022.21.4.a2 D23]),<br />
Multi-Level Modelling Languages <br />
([https://doi.org/10.1016/j.jlamp.2022.100831 RMDRW23],<br />
[https://doi.org/10.1007/s10270-021-00947-1 RDK23]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and <br />
design and verification of the secure-by-construction Illinois’s IBOS browser ([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], <br />
[https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Networks: <br />
AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), <br />
MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), <br />
BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); <br />
DDoS-Intruder models; and <br />
DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): <br />
ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), <br />
Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), <br />
VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool]. <br />
Secure bandwidth reservation in path-aware Internet architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), <br />
end-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]).<br />
SCION’s bandwidth allocation protocol ([https://link.springer.com/book/10.1007/978-3-031-05288-0 CLBHHMP22]).<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2024-03-20T13:58:18Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: full C <br />
([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), <br />
Java <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), <br />
JVM <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), <br />
[https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] <br />
([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), <br />
Verilog <br />
([https://ieeexplore.ieee.org/document/5558634 MKMR10]), <br />
E-LOTOS <br />
([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], <br />
[https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), <br />
UML <br />
([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], <br />
[https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), <br />
MOF <br />
([https://doi.org/10.1007/s00165-009-0140-9 BM10]), <br />
ODP <br />
([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], <br />
[https://doi.org/10.1016/j.csi.2004.10.008 DRV05], <br />
[https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), <br />
AADL <br />
([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], <br />
[https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), <br />
Ptolemy <br />
([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), <br />
BPMN <br />
([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], <br />
[https://doi.org/10.1016/j.scico.2018.08.007 DRS18], <br />
[https://doi.org/10.1007/978-3-031-12441-9_6 DMC23], <br />
[https://doi.org/10.1016/j.jlamp.2023.100928 DPR24]), <br />
DSMLs <br />
([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], <br />
[https://doi.org/10.1177/0037549709341635 RDV09],<br />
[https://doi.org/10.5381/jot.2022.21.4.a2 D23]),<br />
Multi-Level Modelling Languages <br />
([https://doi.org/10.1016/j.jlamp.2022.100831 RMDRW23],<br />
[https://doi.org/10.1007/s10270-021-00947-1 RDK23]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and <br />
design and verification of the secure-by-construction Illinois’s IBOS browser <br />
([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], <br />
[https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Networks: <br />
AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), <br />
MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), <br />
BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); <br />
DDoS-Intruder models; and <br />
DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): <br />
ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), <br />
Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), <br />
VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool]. <br />
Secure bandwidth reservation in path-aware Internet architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), <br />
end-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]).<br />
SCION’s bandwidth allocation protocol ([https://link.springer.com/book/10.1007/978-3-031-05288-0 CLBHHMP22]).<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2024-03-20T13:57:02Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: <br />
full C <br />
([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), <br />
Java <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), <br />
JVM <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), <br />
[https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] <br />
([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), <br />
Verilog <br />
([https://ieeexplore.ieee.org/document/5558634 MKMR10]), <br />
E-LOTOS <br />
([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], <br />
[https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), <br />
UML <br />
([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], <br />
[https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), <br />
MOF <br />
([https://doi.org/10.1007/s00165-009-0140-9 BM10]), <br />
ODP <br />
([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], <br />
[https://doi.org/10.1016/j.csi.2004.10.008 DRV05], <br />
[https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), <br />
AADL <br />
([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], <br />
[https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), <br />
Ptolemy <br />
([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), <br />
BPMN <br />
([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], <br />
[https://doi.org/10.1016/j.scico.2018.08.007 DRS18], <br />
[https://doi.org/10.1007/978-3-031-12441-9_6 DMC23], <br />
[https://doi.org/10.1016/j.jlamp.2023.100928 DPR24]), <br />
DSMLs <br />
([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], <br />
[https://doi.org/10.1177/0037549709341635 RDV09],<br />
[https://doi.org/10.5381/jot.2022.21.4.a2 D23]),<br />
Multi-Level Modelling Languages <br />
([https://doi.org/10.1016/j.jlamp.2022.100831 RMDRW23],<br />
[https://doi.org/10.1007/s10270-021-00947-1 RDK23]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: <br />
uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and <br />
design and verification of the secure-by-construction Illinois’s IBOS browser <br />
([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], <br />
[https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Networks: <br />
AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), <br />
MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), <br />
BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); <br />
DDoS-Intruder models; and <br />
DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): <br />
ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), <br />
Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), <br />
VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool]. <br />
Secure bandwidth reservation in path-aware Internet architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), <br />
end-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]).<br />
SCION’s bandwidth allocation protocol ([https://link.springer.com/book/10.1007/978-3-031-05288-0 CLBHHMP22].<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2024-03-20T13:53:35Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: <br />
full C <br />
([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), <br />
Java <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), <br />
JVM <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), <br />
[https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] <br />
([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), <br />
Verilog <br />
([https://ieeexplore.ieee.org/document/5558634 MKMR10]), <br />
E-LOTOS <br />
([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], <br />
[https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), <br />
UML <br />
([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], <br />
[https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), <br />
MOF <br />
([https://doi.org/10.1007/s00165-009-0140-9 BM10]), <br />
ODP <br />
([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], <br />
[https://doi.org/10.1016/j.csi.2004.10.008 DRV05], <br />
[https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), <br />
AADL <br />
([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], <br />
[https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), <br />
Ptolemy <br />
([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), <br />
BPMN <br />
([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], <br />
[https://doi.org/10.1016/j.scico.2018.08.007 DRS18], <br />
[https://doi.org/10.1007/978-3-031-12441-9_6 DMC23], <br />
[https://doi.org/10.1016/j.jlamp.2023.100928 DPR24]), <br />
DSMLs <br />
([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], <br />
[https://doi.org/10.1177/0037549709341635 RDV09],<br />
[https://doi.org/10.5381/jot.2022.21.4.a2 D23]),<br />
Multi-Level Modelling Languages <br />
([https://doi.org/10.1016/j.jlamp.2022.100831 RMDRW23],<br />
[https://doi.org/10.1007/s10270-021-00947-1 RDK23]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: <br />
uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and <br />
design and verification of the secure-by-construction Illinois’s IBOS browser <br />
([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], <br />
[https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Networks: AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); DDoS-Intruder models; and DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool]. Secure bandwidth reservation in path-aware Internet architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), end-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]).<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2024-03-20T13:52:00Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: <br />
full C <br />
([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), <br />
Java <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), <br />
JVM <br />
([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), <br />
[https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] <br />
([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), <br />
Verilog <br />
([https://ieeexplore.ieee.org/document/5558634 MKMR10]), <br />
E-LOTOS <br />
([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], <br />
[https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), <br />
UML <br />
([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], <br />
[https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), <br />
MOF <br />
([https://doi.org/10.1007/s00165-009-0140-9 BM10]), <br />
ODP <br />
([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], <br />
[https://doi.org/10.1016/j.csi.2004.10.008 DRV05], <br />
[https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), <br />
AADL <br />
([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], <br />
[https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), <br />
Ptolemy <br />
([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), <br />
BPMN <br />
([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], <br />
[https://doi.org/10.1016/j.scico.2018.08.007 DRS18], <br />
[https://doi.org/10.1007/978-3-031-12441-9_6 DMC23], <br />
[https://doi.org/10.1016/j.jlamp.2023.100928 DPR24]), <br />
DSMLs <br />
([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], <br />
[https://doi.org/10.1177/0037549709341635 RDV09],<br />
[https://doi.org/10.5381/jot.2022.21.4.a2 D23]),<br />
Multi-Level Modelling Languages <br />
([https://doi.org/10.1016/j.jlamp.2022.100831 RMDRW23],<br />
[https://doi.org/10.1007/s10270-021-00947-1 RDK23]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: <br />
uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and <br />
design and verification of the secure-by-construction Illinois’s IBOS browser <br />
([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], <br />
[https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Networks: AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); DDoS-Intruder models; and DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool]. Secure bandwidth reservation in path-aware Internet architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), end-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]).<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Maude_Manual_and_ExamplesMaude Manual and Examples2024-03-20T13:38:54Z<p>Malaga: </p>
<hr />
<div>== Manual - Latest Version ==<br />
<br />
The Maude manual for Maude 3.4 is available in [[Media:Maude34manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The source code for the examples used in the manual is also available [[Media:Maude-3.4-manual-book-examples.zip|here]] together with the examples from the Maude book.<br />
<br />
== Additional Resources ==<br />
<br />
Some papers a reports on Maude, its formal foundations, and its applications are available in the [[http://maude.cs.illinois.edu/w/index.php/Some_Papers_on_Maude_and_on_Rewriting_Logic Section on Some Papers on Maude and on Rewriting Logic]].<br />
A primer written for Maude 2.0.1 (but mostly applicable for later versions too) is available in [[Media:Maude-primer.pdf|PDF]] format. <br />
The examples are available as a tarred gzipped [[Media:Maude-primer-Ex.tar.gz|archive]].</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Rewriting_LogicRewriting Logic2024-03-20T13:36:41Z<p>Malaga: </p>
<hr />
<div><br />
The theory and applications of rewriting logic have been vigorously developed <br />
by researchers all over the world during the past years, with more than three <br />
hundred papers related to rewriting logic published so far <br />
(see the [[Roadmap and Bibliography|roadmap]]).<br />
<br />
International workshops on rewriting logic have been held in<br />
[http://www.sciencedirect.com/science/journal/15710661/4 United States (1996)], <br />
[http://www.sciencedirect.com/science/journal/15710661/15 France (1998)], <br />
[http://www.sciencedirect.com/science/journal/15710661/36 Japan (2000)], <br />
[http://www.sciencedirect.com/science/journal/15710661/71 Italy (2002)], <br />
[http://www.sciencedirect.com/science/journal/15710661/117 Spain (2004)],<br />
[http://www.sciencedirect.com/science/journal/15710661/176/4 Austria (2006)],<br />
[http://www.sciencedirect.com/science/journal/15710661/238/3 Hungary (2008)], <br />
[http://link.springer.com/book/10.1007/978-3-642-16310-4/page/1 Cyprus (2010)], <br />
[http://link.springer.com/book/10.1007/978-3-642-34005-5/page/1 Estonia (2012)], <br />
[http://users.dsic.upv.es/workshops/wrla2014/ France (2014)], <br />
[https://fmse.info.uaic.ro/events/WRLA2016/ The Netherlands (2016)], <br />
[https://project.inria.fr/wrla18/ Greece (2018)], <br />
[https://wrla2020.webs.upv.es/ Ireland (2020)],<br />
[http://sv.postech.ac.kr/wrla2022/ Germany (2022)].<br />
<br />
Several journal special issues have been published on rewriting logic:<br />
[https://www.sciencedirect.com/journal/theoretical-computer-science/vol/285/issue/2 TCS 285 (2002)],<br />
[https://link.springer.com/journal/10990/20/1/page/1 HOSC 20 (2007)],<br />
[https://www.sciencedirect.com/journal/the-journal-of-logic-and-algebraic-programming/vol/81 JLAMP 81 (2012)],<br />
[https://www.sciencedirect.com/journal/science-of-computer-programming/vol/99/ SCP 99 (2012)],<br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/vol/85/issue/1/part/P1 JLAMP 85 (2016)],<br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/vol/86/issue/1 JLAMP 86 (2017)], <br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/special-issue/10QHD3B3JSJ JLAMP 93 (2017)], <br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/special-issue/10R8T94S8FM JLAMP 110 (2020)], and <br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/special-issue/10HT7LGD2SQ JLAMP 134 (2023)].<br />
<br />
Furthermore, several language implementations of rewriting logic<br />
([http://www.ldl.jaist.ac.jp/cafeobj/index.html CafeOBJ], [http://elan.loria.fr/ ELAN], [[The Maude System|Maude]], etc.)<br />
and a variety of [[Maude Tools|formal tools]]<br />
have also been developed and have been used in a wide range of applications. <br />
You may take a look to the [https://doi.org/10.1007/978-3-030-17502-3_6 retrospective on rewrite engines published in TACAS 2019].<br />
<br />
Several snapshots of the state of rewriting logic research&mdash;some more global in scope, <br />
and others restricted to specific areas such as concurrency or object-based systems&mdash;have <br />
appeared so far<br />
[https://doi.org/10.1007/3-540-61604-7_64 CONCUR'96],<br />
[http://maude.cs.illinois.edu/papers/abstract/Mdirections_1998.html Marktoberdorf'98],<br />
[https://doi.org/10.1007/10721975_1 RTA'00],<br />
[https://doi.org/10.1007/978-0-387-35520-7_5 FMOODS'00], <br />
[http://maude.cs.illinois.edu/papers/abstract/MMroadmap_2001.html TCS'02],<br />
[https://doi.org/10.1016/j.jlap.2012.06.003 JLAMP'12], <br />
[https://doi.org/10.1007/978-3-662-57669-4_2 WoLLIC'18], <br />
[https://doi.org/10.1016/j.jlamp.2019.100497 JLAMP'20], and<br />
[https://doi.org/10.1007/978-3-031-10769-6_31 IJCAR'22].<br />
<br />
Maude should be seen as our contribution to the broader<br />
collective effort of building good language implementations for<br />
rewriting logic. In this regard, a key distinguishing feature of<br />
Maude is its systematic and efficient use of <EM>reflection</EM>,<br />
exploiting the fact that rewriting logic is reflective, a feature that<br />
makes Maude remarkably extensible and powerful, and that allows many<br />
advanced metaprogramming and metalanguage applications.<br />
<br />
Several versions of Maude have also been presented in different venues: <br />
[https://doi.org/10.1007/3-540-48685-2_18 RTA'99],<br />
[https://doi.org/10.1016/S1571-0661(05)80137-9 WRLA'00],<br />
[https://doi.org/10.1007/3-540-44881-0_7 RTA'03],<br />
[https://doi.org/10.1007/978-3-642-02348-4_27 RTA'04],<br />
[https://doi.org/10.4230/LIPIcs.RTA.2011.31 RTA'11],<br />
[https://doi.org/10.1007/978-3-319-40229-1_13 IJCAR'16], and<br />
[https://doi.org/10.1007/978-3-031-10769-6_31 IJCAR'22].<br />
An account of the history of the language may be found in the [https://doi.org/10.1007/978-3-319-23165-5_11 Two Decades of Maude] 2015 paper.<br />
Some more recent papers have focused on specific aspects of the language:<br />
[https://doi.org/10.1016/j.jlamp.2023.100887 strategies],<br />
[https://doi.org/10.1007/978-3-031-10769-6_31 symbolic features].</div>Malagahttps://maude.cs.illinois.edu/w/index.php/The_Maude_SystemThe Maude System2024-03-20T13:32:48Z<p>Malaga: </p>
<hr />
<div><!--[[File:Maude-logo.png|right|400px]]--><br />
[[File:streets-cross.png|right|400px|thumb|link=https://www.google.com/maps/@37.392819,-122.0391638,3a,15y,246.71h,88.08t/data=!3m6!1e1!3m4!1sJ2um6VisMqkDoFT4Lpyd7A!2e0!7i16384!8i8192|[https://www.google.com/maps/@37.392819,-122.0391638,3a,15y,246.71h,88.08t/data=!3m6!1e1!3m4!1sJ2um6VisMqkDoFT4Lpyd7A!2e0!7i16384!8i8192 Streets cross at Sunnyvale, CA]]]<br />
<br />
== General Maude Information ==<br />
* [[Maude Overview]]<br />
* [[The Maude Project and Team]]<br />
* [[Rewriting Logic]]<br />
* [[Maude Mailing Addresses and Lists|Bug Reports and Mailing Lists]]<br />
<br />
== Maude Documentation ==<br />
<br />
* [[Maude Manual and Examples|Maude Manual and Examples]]<br />
* [[Some Papers on Maude and on Rewriting Logic|Some Papers on Maude and on Rewriting Logic]]<br />
<!-- * [http://maude.cs.illinois.edu/papers/ Some Papers on Maude and on Rewriting Logic] --><br />
<!-- * [[Roadmap and Bibliography]] --><br />
<!-- * [[Some Talks on Maude and on Rewriting Logic]] --><br />
<!-- * [[Maude 2 Primer and Examples|Maude Primer and Examples (not maintained)]] --><br />
<br />
== Maude-related Tools and Applications==<br />
* [[Maude Tools]]<br />
* [[Applications]]<br />
<br />
== Obtaining and Using Maude ==<br />
<br />
* [[Maude download and installation|Maude download and installation]]<br />
* [[Maude License Agreement|Maude 3 License]]<br />
* [[All Maude 3 versions|All Maude 3 versions]]<br />
* [[All Maude 2 versions|All Maude 2 versions]]<br />
* [http://maude.cs.uiuc.edu/maude1/ Looking for Maude 1?]</div>Malagahttps://maude.cs.illinois.edu/w/index.php/File:Maude-3.4-manual-book-examples.zipFile:Maude-3.4-manual-book-examples.zip2024-03-19T12:09:19Z<p>Malaga: </p>
<hr />
<div></div>Malagahttps://maude.cs.illinois.edu/w/index.php/Maude_Manual_and_ExamplesMaude Manual and Examples2024-03-17T20:15:26Z<p>Malaga: </p>
<hr />
<div>== Manual - Latest Version ==<br />
<br />
The Maude manual for Maude 3.4 is available in [[Media:Maude34manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The source code for the examples used in the manual is also available [[Media:Maude-3.4-manual-book-examples.zip|here]] together with the examples from the Maude book.<br />
<br />
The Maude manual for Maude 3.3.1 is available in [[Media:Maude-3.3.1-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The source code for the examples used in the manual is also available [[Media:Maude-3.3.1-manual-book-examples.zip|here]] together with the examples from the Maude book.<br />
<br />
== Additional Resources ==<br />
<br />
Some papers a reports on Maude, its formal foundations, and its applications are available in the [[http://maude.cs.illinois.edu/w/index.php/Some_Papers_on_Maude_and_on_Rewriting_Logic Section on Some Papers on Maude and on Rewriting Logic]].<br />
A primer written for Maude 2.0.1 (but mostly applicable for later versions too) is available in [[Media:Maude-primer.pdf|PDF]] format. <br />
The examples are available as a tarred gzipped [[Media:Maude-primer-Ex.tar.gz|archive]].</div>Malagahttps://maude.cs.illinois.edu/w/index.php/File:Maude34manual.pdfFile:Maude34manual.pdf2024-03-17T20:14:20Z<p>Malaga: </p>
<hr />
<div></div>Malagahttps://maude.cs.illinois.edu/w/index.php/Maude_Manual_and_ExamplesMaude Manual and Examples2024-03-17T20:11:28Z<p>Malaga: </p>
<hr />
<div>== Manual - Latest Version ==<br />
<br />
The Maude manual for Maude 3.4 is available in [[Media:Maude34-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The source code for the examples used in the manual is also available [[Media:Maude-3.4-manual-book-examples.zip|here]] together with the examples from the Maude book.<br />
<br />
The Maude manual for Maude 3.3.1 is available in [[Media:Maude-3.3.1-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The source code for the examples used in the manual is also available [[Media:Maude-3.3.1-manual-book-examples.zip|here]] together with the examples from the Maude book.<br />
<br />
== Additional Resources ==<br />
<br />
Some papers a reports on Maude, its formal foundations, and its applications are available in the [[http://maude.cs.illinois.edu/w/index.php/Some_Papers_on_Maude_and_on_Rewriting_Logic Section on Some Papers on Maude and on Rewriting Logic]].<br />
A primer written for Maude 2.0.1 (but mostly applicable for later versions too) is available in [[Media:Maude-primer.pdf|PDF]] format. <br />
The examples are available as a tarred gzipped [[Media:Maude-primer-Ex.tar.gz|archive]].</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Maude_Manual_and_ExamplesMaude Manual and Examples2024-03-17T20:07:33Z<p>Malaga: </p>
<hr />
<div>== Manual - Latest Version ==<br />
<br />
The Maude manual for Maude 3.4 is available in [[Media:Maude-3.4-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The source code for the examples used in the manual is also available [[Media:Maude-3.4-manual-book-examples.zip|here]] together with the examples from the Maude book.<br />
<br />
The Maude manual for Maude 3.3.1 is available in [[Media:Maude-3.3.1-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The source code for the examples used in the manual is also available [[Media:Maude-3.3.1-manual-book-examples.zip|here]] together with the examples from the Maude book.<br />
<br />
== Additional Resources ==<br />
<br />
Some papers a reports on Maude, its formal foundations, and its applications are available in the [[http://maude.cs.illinois.edu/w/index.php/Some_Papers_on_Maude_and_on_Rewriting_Logic Section on Some Papers on Maude and on Rewriting Logic]].<br />
A primer written for Maude 2.0.1 (but mostly applicable for later versions too) is available in [[Media:Maude-primer.pdf|PDF]] format. <br />
The examples are available as a tarred gzipped [[Media:Maude-primer-Ex.tar.gz|archive]].</div>Malagahttps://maude.cs.illinois.edu/w/index.php/File:Maude-manual-34.pdfFile:Maude-manual-34.pdf2024-03-17T20:05:36Z<p>Malaga: Maude Manual 3.4</p>
<hr />
<div>Maude Manual 3.4</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2023-12-14T11:20:20Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: full C ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), Java ([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), JVM ([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), [https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] ([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), Verilog ([https://ieeexplore.ieee.org/document/5558634 MKMR10]), E-LOTOS ([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], [https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), UML ([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], [https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), MOF ([https://doi.org/10.1007/s00165-009-0140-9 BM10]), ODP ([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], [https://doi.org/10.1016/j.csi.2004.10.008 DRV05], [https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), AADL ([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], [https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), Ptolemy ([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), BPMN ([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], [https://doi.org/10.1016/j.scico.2018.08.007 DRS18]), and DSMLs ([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], [https://doi.org/10.1177/0037549709341635 RDV09]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and design and verification of the secure-by-construction Illinois’s IBOS browser ([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], [https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Networks: AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); DDoS-Intruder models; and DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool]. Secure bandwidth reservation in path-aware Internet architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), end-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]).<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2023-12-14T11:19:32Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: full C ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), Java ([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), JVM ([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), [https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] ([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), Verilog ([https://ieeexplore.ieee.org/document/5558634 MKMR10]), E-LOTOS ([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], [https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), UML ([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], [https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), MOF ([https://doi.org/10.1007/s00165-009-0140-9 BM10]), ODP ([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], [https://doi.org/10.1016/j.csi.2004.10.008 DRV05], [https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), AADL ([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], [https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), Ptolemy ([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), BPMN ([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], [https://doi.org/10.1016/j.scico.2018.08.007 DRS18]), and DSMLs ([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], [https://doi.org/10.1177/0037549709341635 RDV09]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and design and verification of the secure-by-construction Illinois’s IBOS browser ([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], [https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Networks: AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); DDoS-Intruder models; and DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool]. Secure Bandwidth Reservation in Path-Aware Internet Architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), End-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]).<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2023-12-14T11:15:46Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: full C ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), Java ([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), JVM ([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), [https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] ([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), Verilog ([https://ieeexplore.ieee.org/document/5558634 MKMR10]), E-LOTOS ([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], [https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), UML ([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], [https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), MOF ([https://doi.org/10.1007/s00165-009-0140-9 BM10]), ODP ([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], [https://doi.org/10.1016/j.csi.2004.10.008 DRV05], [https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), AADL ([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], [https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), Ptolemy ([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), BPMN ([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], [https://doi.org/10.1016/j.scico.2018.08.007 DRS18]), and DSMLs ([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], [https://doi.org/10.1177/0037549709341635 RDV09]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and design and verification of the secure-by-construction Illinois’s IBOS browser ([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], [https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Network protocols: AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); DDoS-Intruder models; and DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool].<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Networking: Secure Bandwidth Reservation in Path-Aware Internet Architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]), End-to-end name resolution ([https://dl.acm.org/doi/abs/10.1145/3603269.3604870 LDHBVBP23]).<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2023-12-13T11:07:06Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: full C ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), Java ([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), JVM ([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), [https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] ([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), Verilog ([https://ieeexplore.ieee.org/document/5558634 MKMR10]), E-LOTOS ([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], [https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), UML ([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], [https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), MOF ([https://doi.org/10.1007/s00165-009-0140-9 BM10]), ODP ([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], [https://doi.org/10.1016/j.csi.2004.10.008 DRV05], [https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), AADL ([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], [https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), Ptolemy ([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), BPMN ([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], [https://doi.org/10.1016/j.scico.2018.08.007 DRS18]), and DSMLs ([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], [https://doi.org/10.1177/0037549709341635 RDV09]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and design and verification of the secure-by-construction Illinois’s IBOS browser ([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], [https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Network protocols: AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); DDoS-Intruder models; and DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool].<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [https://pubmed.ncbi.nlm.nih.gov/11928493/ EKLLMS02].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Networking security: N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]).<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/ApplicationsApplications2023-12-13T11:06:04Z<p>Malaga: </p>
<hr />
<div>Maude and its formal tools have been used in many pioneering applications: <br />
<br />
* Formal definition and verification of programming and hardware, resp. software, modeling languages: full C ([https://dl.acm.org/doi/10.1145/2103621.2103719 ER12]), Java ([https://link.springer.com/chapter/10.1007/978-3-540-27813-9_46 FCMR04]), JVM ([https://link.springer.com/chapter/10.1007/978-3-540-27815-3_14 FMR04]), [https://shemesh.larc.nasa.gov/fm/PLEXIL/ NASA’s PLEXIL] ([https://link.springer.com/chapter/10.1007%2F978-3-642-30729-4_24 RCMS12]), Verilog ([https://ieeexplore.ieee.org/document/5558634 MKMR10]), E-LOTOS ([https://link.springer.com/chapter/10.1007%2F3-540-36135-9_19 V02], [https://link.springer.com/article/10.1007/s10703-005-2254-x VM05]), UML ([https://link.springer.com/chapter/10.1007%2F11784180_28 CE06], [https://doi.org/10.1007/978-3-642-54624-2_11 DRMA14]), MOF ([https://doi.org/10.1007/s00165-009-0140-9 BM10]), ODP ([https://doi.org/10.1016/S0920-5489(02)00121-6 DV03], [https://doi.org/10.1016/j.csi.2004.10.008 DRV05], [https://doi.org/10.1016/j.csi.2006.11.004 RVD07]), AADL ([https://doi.org/10.1007/978-3-642-13464-7_5 OBM10], [https://doi.org/10.1007/978-3-319-06410-9_7 BOM14]), Ptolemy ([https://www.sciencedirect.com/science/article/pii/S0167642310001863 BOFLT14]), BPMN ([https://doi.org/10.1007/978-3-319-59746-1_12 DS17], [https://doi.org/10.1016/j.scico.2018.08.007 DRS18]), and DSMLs ([https://doi.org/10.5381/jot.2007.6.9.a10 RRDV], [https://doi.org/10.1177/0037549709341635 RDV09]).<br />
<br />
* Semantics of hardware architectures: MCA ARMv8 architecture ([https://www.sciencedirect.com/science/article/pii/S1383762122000352 XZ22]). <br />
<br />
* Browser security: uncovering 12 kinds of unknown attacks on Internet Explorer ([https://ieeexplore.ieee.org/abstract/document/4223215 CMSWW07]), and design and verification of the secure-by-construction Illinois’s IBOS browser ([https://link.springer.com/chapter/10.1007/978-3-642-35861-6_14 SKMT12], [https://link.springer.com/chapter/10.1007%2F978-3-030-63595-4_10 SMR20]).<br />
<br />
* Cryptographic protocol analysis: [http://maude.cs.illinois.edu/w/index.php/Maude_Tools:_Maude-NPA Maude-NPA] has analyzed many protocols and crypto-APIs modulo algebraic properties, like Yubikey&YubiHSM ([https://easychair.org/publications/paper/qkkq GAEMM18]), IBM’s CCA ([https://link.springer.com/chapter/10.1007/978-3-319-14054-4_8 GSEMM14]), and PCKS#11 ([https://link.springer.com/chapter/10.1007/978-3-319-27152-1_5 GSEMM15]), using unification and symbolic reachability. See [https://doi.org/10.1007/978-3-642-03829-7_1 EMM09]. An account of the NRL protocol analyzer can be found [https://doi.org/10.1016/j.tcs.2006.08.035 here]. [https://tamarin-prover.github.io/ Tamarin] at ETH, resp. [https://github.com/akiss/akiss AKISS] at INRIA, use Maude’s unification to analyze protocols like 5G-AKA ([https://people.cispa.io/cas.cremers/tamarin/5G/ DC18]), resp. RFID ([https://link.springer.com/chapter/10.1007/978-3-319-66399-9_1 GK17]).<br />
<br />
* Network protocols: AER/NCA active networks ([https://link.springer.com/chapter/10.1007/3-540-45314-8_24 OKMTZ06]), MANETS ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]), BGP ([https://repository.upenn.edu/cgi/viewcontent.cgi?article=2029&context=cis_reports Wetal13], [https://link.springer.com/chapter/10.1007/978-3-642-21461-5_22 Wetal11], [https://link.springer.com/chapter/10.1007/978-3-642-28756-5_20 WTGLS12]); DDoS-Intruder models; and DDoS protection ([https://www.sciencedirect.com/science/article/pii/S2352220816301651 LDFN18]): ASV ([https://www.sciencedirect.com/science/article/pii/S1571066109000747 AMG09]), Stable Availability ([http://dx.doi.org/10.1007/978-3-642-28872-2_6 EMMW12]), VoIP-SIP ([https://link.springer.com/chapter/10.1007/978-3-642-04444-1_24 SASGM09]), using [http://maude.cs.uiuc.edu/tools/pvesta/ Maude’s statistical model checking (SMC) tool].<br />
<br />
* Cloud transaction system formalization and analysis: Cassandra ([https://dl.acm.org/doi/10.1007/978-3-319-22264-6_15 LNGRG15]), Google’s Megastore ([https://link.springer.com/chapter/10.1007%2F978-3-319-10431-7_12 GO14]), P-Store ([https://link.springer.com/chapter/10.1007/978-3-319-72044-9_13 O17]), etc. ([https://onlinelibrary.wiley.com/doi/10.1002/9781119428497.ch2 Betal18]), using SMC.<br />
<br />
* Analysis of real-time and cyber-physical systems: CASH scheduling ([https://link.springer.com/chapter/10.1007/11693017_26 OC06]), sensor ([https://www.sciencedirect.com/science/article/pii/S0304397508006683 OT09]) and MANET ([https://www.sciencedirect.com/science/article/pii/S2352220815000498 LOM16]) networks, timed security protocols ([https://link.springer.com/chapter/10.1007%2F978-3-030-65277-7_7 AEMMS20]), PALS transformation from synchronous to correct distributed real-time systems ([http://dx.doi.org/10.1016/j.tcs.2012.05.040 MO12], [https://link.springer.com/chapter/10.1007/978-3-642-35861-6_1 BMO12]) enables model checking of complex models such as AADL and Ptolemy models ([https://link.springer.com/chapter/10.1007/978-3-319-06410-9_7 BOM14]) and distributed control of airplane maneuvers ([http://dx.doi.org/10.4204/EPTCS.105.2 BKMO12]).<br />
<br />
* Models of cell signaling used to explain drug effects, identify pathogen attack surfaces, etc. ([http://pl.csl.sri.com/ Pathway Logic]). See [EKLLMS02 https://pubmed.ncbi.nlm.nih.gov/11928493/].<br />
<br />
* Specification and analysis of models of Concurrency: Petri Nets ([https://link.springer.com/chapter/10.1007/3-540-45541-8_9 SMO01]), CCS, pi-Calculus ([https://www.sciencedirect.com/science/article/pii/S1571066105801252 S00]), Actors ([https://mitpress.mit.edu/books/research-directions-concurrent-object-oriented-programming M93]), REO ([https://doi.org/10.1016/j.entcs.2005.12.034 MSA]), Orc ([https://www.sciencedirect.com/science/article/pii/S2352220815000334 AM15]). <br />
<br />
* Logical framework applications to prototype logics and build and interoperate theorem provers: Barendregt’s lambda-cube ([https://link.springer.com/chapter/10.1007/978-3-540-39993-3_16 SM04]), linear logic ([https://link.springer.com/chapter/10.1007/978-94-017-0464-9_1 MM02]), modal logics ([https://link.springer.com/chapter/10.1007/978-3-319-99840-4_7 OPR18]), computational algebraic geometry, Maude’s Church-Rosser Checker and Inductive ([https://www.sciencedirect.com/science/article/pii/S1567832611001147 DM12], [https://doi.org/10.1016/j.jlamp.2019.100513 DMR20]) and Reachability Logic ([https://link.springer.com/chapter/10.1007/978-3-319-94460-9_12 SSM17]), theorem provers, HOL-to-Nuprl translator ([https://link.springer.com/chapter/10.1007/3-540-44755-5_23 NSM01]), integration of logic and deep-learning, etc. These applications use meta-level, search, and symbolic features.<br />
<br />
* Networking security: N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures ([https://zenodo.org/record/5856306#.YgTkifXMLt0 WLSPB22]).<br />
<br />
* Distributed databases: SNOW-Optimal Read Atomic Transactions ([https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/511821/1/main.pdf L22]), Replicated RAMP Transactions ([https://ieeexplore.ieee.org/abstract/document/9546747 LL21]).<br />
<br />
* IoT systems: Attack Surface of Trigger-Action IoT Platforms ([https://dl.acm.org/doi/abs/10.1145/3319535.3345662 WDYLBG19]), Automated Composition, Analysis and Deployment of IoT Applications ([https://doi.org/10.1007/978-3-030-29852-4_21 DG19]).<br />
<br />
* Runtime verification: See works by [https://doi.org/10.1007/s10515-005-6205-y Roşu and Havelund].<br />
<br />
Please, help us to complete this page. If you know of applications that should be in this list, email us to duran(at)lcc(dot)uma(dot)es.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Some_Papers_on_Maude_and_on_Rewriting_LogicSome Papers on Maude and on Rewriting Logic2023-12-13T10:47:41Z<p>Malaga: </p>
<hr />
<div>A friendly introduction to the latest advances in the symbolic features of Maude will appear in Proc. LOPSTER 2020: [[Media:maude-tapas.pdf|Symbolic Computation in Maude: Some Tapas]].<br />
<br />
In-depth presentations of Maude, and on how to use its most common features, are available in the following books: <br />
<br />
* M. Clavel et al.: [https://doi.org/10.1007/978-3-540-71999-1 All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic]. LNCS 4350, Springer (2007)<br />
<br />
* P.C. Ölveczky: [https://doi.org/10.1007/978-1-4471-6687-0 Designing Reliable Distributed Systems - A Formal Methods Approach Based on Executable Modeling in Maude]. Springer (2017)<br />
<br />
Several bibliographies and surveys on rewriting logic and Maude have been published:<br />
<br />
* M. Clavel et al.: [https://doi.org/10.1007/978-3-319-23165-5_11 Two Decades of Maude]. Logic, Rewriting, and Concurrency: 232-254 (2015). A pre-print is available [[Media:Two-Decades-of-Maude.pdf|here]].<br />
<br />
* J. Meseguer: [https://doi.org/10.1016/j.jlap.2012.06.003 Twenty years of rewriting logic]. J. Log. Algebraic Methods Program. 81(7-8): 721-781 (2012). A pre-print is available [[Media:20-years.pdf|here]].<br />
<br />
* N. Martí-Oliet, M. Palomino, and A. Verdejo: [https://www.sciencedirect.com/science/article/pii/S1567832612000562?via%3Dihub Rewriting logic bibliography by topic: 1990–2011]. J. Log. Algebraic Methods Program. 81: 782-815 (2012)<br />
<br />
* N. Martí-Oliet and J. Meseguer: [https://www.sciencedirect.com/science/article/pii/S0304397501003577 Rewriting logic: roadmap and bibliography]. Theor. Comput. Sci. 285(2): 121-154 (2002). A pre-print is available [[Media:MMroadmap_2001.pdf|here]].<br />
<br />
The following papers may serve as a selection of such huge body of work:<br />
<br />
* S. Liu et al.: [https://doi.org/10.1145/3563299 Bridging the semantic gap between qualitative and quantitative models of distributed systems]. Proc. ACM Program. Lang. 6 (OOPSLA2): 315-344 (2022)<br />
<br />
* F. Durán et al.: [https://doi.org/10.1016/j.jlamp.2019.100497 Programming and symbolic computation in Maude]. J. Log. Algebraic Methods Program. 110 (2020). A pre-print is available [[Media:maude-jlamp.pdf|here]].<br />
<br />
* J. Meseguer: [https://doi.org/10.1016/j.jlamp.2019.100483 Generalized rewrite theories, coherence completion, and symbolic methods]. J. Log. Algebraic Methods Program. 110 (2020). A pre-print is available [[Media:BMgrt_2003.pdf|here]].<br />
<br />
* F. Durán, J. Meseguer, and C. Rocha: [https://doi.org/10.1016/j.jlamp.2019.100513 Ground confluence of order-sorted conditional specifications modulo axioms]. J. Log. Algebraic Methods Program. 111: 100513 (2020). A pre-print is available [[Media:Durán.Mesegue.Rocha.Ground Confluence of Order-sorted Conditional Specifications Modulo Axioms.TR.pdf|here]].<br />
<br />
* C. Rocha, J. Meseguer, C. Muñoz: [https://doi.org/10.1016/j.jlamp.2016.10.001 Rewriting modulo SMT and open system analysis]. J. Log. Algebraic Methods Program. 86(1): 269-297 (2017)<br />
<br />
* S. Escobar, R. Sasse, J. Meseguer: [https://doi.org/10.1016/j.jlap.2012.01.002 Folding variant narrowing and optimal variant termination]. J. Log. Algebraic Methods Program. 81(7-8): 898-928 (2012)<br />
<br />
* F. Durán and J. Meseguer: [https://doi.org/10.1016/j.jlap.2011.12.004 On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories]. J. Log. Algebraic Methods Program. 81(7-8): 816-850 (2012). A pre-print is available [[Media:CRChC.pdf|here]].<br />
<br />
* J. Meseguer, M. Palomino, and N. Martí-Oliet: [https://doi.org/10.1016/j.jlap.2009.07.003 Algebraic simulations]. J. Log. Algebraic Methods Program. 79(2): 103-143 (2010). A pre-print is available [[Media:MartiOlietEtAl03-journal.pdf|here]].<br />
<br />
* J. Meseguer, M. Palomino, and N. Martí-Oliet: [https://doi.org/10.1016/j.tcs.2008.04.040 Equational abstractions]. Theor. Comput. Sci. 403(2-3): 239-264 (2008). A pre-print is available [[Media:MPMea_2003.pdf|here]].<br />
<br />
* M. Clavel, J. Meseguer, and M. Palomino: [https://doi.org/10.1016/j.tcs.2006.12.009 Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic]. Theor. Comput. Sci. 373(1-2): 70-91 (2007)<br />
<br />
* P.C. Ölveczky and J. Meseguer: [https://doi.org/10.1007/s10990-007-9001-5 Semantics and pragmatics of Real-Time Maude]. High. Order Symb. Comput. 20(1-2): 161-196 (2007)<br />
<br />
* F. Durán and J. Meseguer: [https://doi.org/10.1016/j.scico.2006.07.002 Maude's module algebra]. Sci. Comput. Program. 66(2): 125-153 (2007)<br />
<br />
* R. Bruni and J. Meseguer: [https://doi.org/10.1016/j.tcs.2006.04.012 Semantic foundations for generalized rewrite theories]. Theor. Comput. Sci. 360(1-3): 386-414 (2006)<br />
<br />
* M. Clavel et al.: [https://doi.org/10.1016/S0304-3975(01)00359-0 Maude: specification and programming in rewriting logic]. Theor. Comput. Sci. 285(2): 187-243 (2002). A pre-print is available [[Media:CDELMMQspecprog_2001.pdf|here]].<br />
<br />
* J. Meseguer: [https://doi.org/10.1007/3-540-64299-4_26 Membership algebra as a logical framework for equational specification]. WADT: 18-61 (1997)<br />
<br />
* N. Martí-Oliet and J. Meseguer: [https://doi.org/10.1016/S1571-0661(04)00040-4 Rewriting logic as a logical and semantic framework]. WRLA: 190-225 (1996)<br />
<br />
* J. Meseguer: [https://www.sciencedirect.com/science/article/pii/030439759290182F Conditional rewriting logic as a unified model of concurrency]. Theor. Comput. Sci. 96(1): 73-155 (1996)<br />
<br />
Some Additional Papers on Maude and on Rewriting Logic are available [http://maude.cs.illinois.edu/papers/ here].</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Some_Papers_on_Maude_and_on_Rewriting_LogicSome Papers on Maude and on Rewriting Logic2023-12-13T10:37:20Z<p>Malaga: </p>
<hr />
<div>A friendly introduction to the latest advances in the symbolic features of Maude will appear in Proc. LOPSTER 2020: [[Media:maude-tapas.pdf|Symbolic Computation in Maude: Some Tapas]].<br />
<br />
In-depth presentations of Maude, and on how to use its most common features, are available in the following books: <br />
<br />
* M. Clavel et al.: [https://doi.org/10.1007/978-3-540-71999-1 All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic]. LNCS 4350, Springer (2007)<br />
<br />
* P.C. Ölveczky: [https://doi.org/10.1007/978-1-4471-6687-0 Designing Reliable Distributed Systems - A Formal Methods Approach Based on Executable Modeling in Maude]. Springer (2017)<br />
<br />
Several bibliographies and surveys on rewriting logic and Maude have been published:<br />
<br />
* M. Clavel et al.: [https://doi.org/10.1007/978-3-319-23165-5_11 Two Decades of Maude]. Logic, Rewriting, and Concurrency: 232-254 (2015). A pre-print is available [[Media:Two-Decades-of-Maude.pdf|here]].<br />
<br />
* J. Meseguer: [https://doi.org/10.1016/j.jlap.2012.06.003 Twenty years of rewriting logic]. J. Log. Algebraic Methods Program. 81(7-8): 721-781 (2012). A pre-print is available [[Media:20-years.pdf|here]].<br />
<br />
* N. Martí-Oliet, M. Palomino, and A. Verdejo: [https://www.sciencedirect.com/science/article/pii/S1567832612000562?via%3Dihub Rewriting logic bibliography by topic: 1990–2011]. J. Log. Algebraic Methods Program. 81: 782-815 (2012)<br />
<br />
* N. Martí-Oliet and J. Meseguer: [https://www.sciencedirect.com/science/article/pii/S0304397501003577 Rewriting logic: roadmap and bibliography]. Theor. Comput. Sci. 285(2): 121-154 (2002). A pre-print is available [[Media:MMroadmap_2001.pdf|here]].<br />
<br />
The following papers may serve as a selection of such huge body of work:<br />
<br />
* F. Durán et al.: [https://doi.org/10.1016/j.jlamp.2019.100497 Programming and symbolic computation in Maude]. J. Log. Algebraic Methods Program. 110 (2020). A pre-print is available [[Media:maude-jlamp.pdf|here]].<br />
<br />
* J. Meseguer: [https://doi.org/10.1016/j.jlamp.2019.100483 Generalized rewrite theories, coherence completion, and symbolic methods]. J. Log. Algebraic Methods Program. 110 (2020). A pre-print is available [[Media:BMgrt_2003.pdf|here]].<br />
<br />
* F. Durán, J. Meseguer, and C. Rocha: [https://doi.org/10.1016/j.jlamp.2019.100513 Ground confluence of order-sorted conditional specifications modulo axioms]. J. Log. Algebraic Methods Program. 111: 100513 (2020). A pre-print is available [[Media:Durán.Mesegue.Rocha.Ground Confluence of Order-sorted Conditional Specifications Modulo Axioms.TR.pdf|here]].<br />
<br />
* C. Rocha, J. Meseguer, C. Muñoz: [https://doi.org/10.1016/j.jlamp.2016.10.001 Rewriting modulo SMT and open system analysis]. J. Log. Algebraic Methods Program. 86(1): 269-297 (2017)<br />
<br />
* S. Escobar, R. Sasse, J. Meseguer: [https://doi.org/10.1016/j.jlap.2012.01.002 Folding variant narrowing and optimal variant termination]. J. Log. Algebraic Methods Program. 81(7-8): 898-928 (2012)<br />
<br />
* F. Durán and J. Meseguer: [https://doi.org/10.1016/j.jlap.2011.12.004 On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories]. J. Log. Algebraic Methods Program. 81(7-8): 816-850 (2012). A pre-print is available [[Media:CRChC.pdf|here]].<br />
<br />
* J. Meseguer, M. Palomino, and N. Martí-Oliet: [https://doi.org/10.1016/j.jlap.2009.07.003 Algebraic simulations]. J. Log. Algebraic Methods Program. 79(2): 103-143 (2010). A pre-print is available [[Media:MartiOlietEtAl03-journal.pdf|here]].<br />
<br />
* J. Meseguer, M. Palomino, and N. Martí-Oliet: [https://doi.org/10.1016/j.tcs.2008.04.040 Equational abstractions]. Theor. Comput. Sci. 403(2-3): 239-264 (2008). A pre-print is available [[Media:MPMea_2003.pdf|here]].<br />
<br />
* M. Clavel, J. Meseguer, and M. Palomino: [https://doi.org/10.1016/j.tcs.2006.12.009 Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic]. Theor. Comput. Sci. 373(1-2): 70-91 (2007)<br />
<br />
* P.C. Ölveczky and J. Meseguer: [https://doi.org/10.1007/s10990-007-9001-5 Semantics and pragmatics of Real-Time Maude]. High. Order Symb. Comput. 20(1-2): 161-196 (2007)<br />
<br />
* F. Durán and J. Meseguer: [https://doi.org/10.1016/j.scico.2006.07.002 Maude's module algebra]. Sci. Comput. Program. 66(2): 125-153 (2007)<br />
<br />
* R. Bruni and J. Meseguer: [https://doi.org/10.1016/j.tcs.2006.04.012 Semantic foundations for generalized rewrite theories]. Theor. Comput. Sci. 360(1-3): 386-414 (2006)<br />
<br />
* M. Clavel et al.: [https://doi.org/10.1016/S0304-3975(01)00359-0 Maude: specification and programming in rewriting logic]. Theor. Comput. Sci. 285(2): 187-243 (2002). A pre-print is available [[Media:CDELMMQspecprog_2001.pdf|here]].<br />
<br />
* J. Meseguer: [https://doi.org/10.1007/3-540-64299-4_26 Membership algebra as a logical framework for equational specification]. WADT: 18-61 (1997)<br />
<br />
* N. Martí-Oliet and J. Meseguer: [https://doi.org/10.1016/S1571-0661(04)00040-4 Rewriting logic as a logical and semantic framework]. WRLA: 190-225 (1996)<br />
<br />
* J. Meseguer: [https://www.sciencedirect.com/science/article/pii/030439759290182F Conditional rewriting logic as a unified model of concurrency]. Theor. Comput. Sci. 96(1): 73-155 (1996)<br />
<br />
Some Additional Papers on Maude and on Rewriting Logic are available [http://maude.cs.illinois.edu/papers/ here].</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Some_Papers_on_Maude_and_on_Rewriting_LogicSome Papers on Maude and on Rewriting Logic2023-12-11T10:21:11Z<p>Malaga: </p>
<hr />
<div>A friendly introduction to the latest advances in the symbolic features of Maude will appear in Proc. LOPSTER 2020: [[Media:maude-tapas.pdf|Symbolic Computation in Maude: Some Tapas]].<br />
<br />
In-depth presentations of Maude, and on how to use its most common features, are available in the following books: <br />
<br />
* M. Clavel et al.: [https://doi.org/10.1007/978-3-540-71999-1 All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic]. LNCS 4350, Springer (2007)<br />
<br />
* P.C. Ölveczky: [https://doi.org/10.1007/978-1-4471-6687-0 Designing Reliable Distributed Systems - A Formal Methods Approach Based on Executable Modeling in Maude]. Springer (2017)<br />
<br />
Several bibliographies and surveys on rewriting logic and Maude have been published:<br />
<br />
* M. Clavel et al.: [https://doi.org/10.1007/978-3-319-23165-5_11 Two Decades of Maude]. Logic, Rewriting, and Concurrency: 232-254 (2015). A pre-print is available [[Media:Two-Decades-of-Maude.pdf|here]].<br />
<br />
* J. Meseguer: [https://doi.org/10.1016/j.jlap.2012.06.003 Twenty years of rewriting logic]. J. Log. Algebraic Methods Program. 81(7-8): 721-781 (2012). A pre-print is available [[Media:20-years.pdf|here]].<br />
<br />
* N. Martí-Oliet, M. Palomino, and A. Verdejo: [https://www.sciencedirect.com/science/article/pii/S1567832612000562?via%3Dihub Rewriting logic bibliography by topic: 1990–2011]. J. Log. Algebraic Methods Program. 81: 782-815 (2012)<br />
<br />
* N. Martí-Oliet and J. Meseguer: [https://www.sciencedirect.com/science/article/pii/S0304397501003577 Rewriting logic: roadmap and bibliography]. Theor. Comput. Sci. 285(2): 121-154 (2002). A pre-print is available [[Media:MMroadmap_2001.pdf|here]].<br />
<br />
The following papers may serve as a selection of such huge body of work:<br />
<br />
* F. Durán et al.: [https://doi.org/10.1016/j.jlamp.2019.100497 Programming and symbolic computation in Maude]. J. Log. Algebraic Methods Program. 110 (2020). A pre-print is available [[Media:maude-jlamp.pdf|here]].<br />
<br />
* J. Meseguer: [https://doi.org/10.1016/j.jlamp.2019.100483 Generalized rewrite theories, coherence completion, and symbolic methods]. J. Log. Algebraic Methods Program. 110 (2020). A pre-print is available [[Media:BMgrt_2003.pdf|here]].<br />
<br />
* F. Durán, J. Meseguer, and C. Rocha: [https://doi.org/10.1016/j.jlamp.2019.100513 Ground confluence of order-sorted conditional specifications modulo axioms]. J. Log. Algebraic Methods Program. 111: 100513 (2020). A pre-print is available [[Media:Durán.Mesegue.Rocha.Ground Confluence of Order-sorted Conditional Specifications Modulo Axioms.TR.pdf|here]].<br />
<br />
* C. Rocha, J. Meseguer, C. Muñoz: [https://doi.org/10.1016/j.jlamp.2016.10.001 Rewriting modulo SMT and open system analysis]. J. Log. Algebraic Methods Program. 86(1): 269-297 (2017)<br />
<br />
* S. Escobar, R. Sasse, J. Meseguer: [https://doi.org/10.1016/j.jlap.2012.01.002 Folding variant narrowing and optimal variant termination]. J. Log. Algebraic Methods Program. 81(7-8): 898-928 (2012)<br />
<br />
* F. Durán and J. Meseguer: [https://doi.org/10.1016/j.jlap.2011.12.004 On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories]. J. Log. Algebraic Methods Program. 81(7-8): 816-850 (2012). A pre-print is available [[Media:CRChC.pdf|here]].<br />
<br />
* J. Meseguer, M. Palomino, and N. Martí-Oliet: [https://doi.org/10.1016/j.jlap.2009.07.003 Algebraic simulations]. J. Log. Algebraic Methods Program. 79(2): 103-143 (2010). A pre-print is available [[Media:MartiOlietEtAl03-journal.pdf|here]].<br />
<br />
* J. Meseguer, M. Palomino, and N. Martí-Oliet: [https://doi.org/10.1016/j.tcs.2008.04.040 Equational abstractions]. Theor. Comput. Sci. 403(2-3): 239-264 (2008). A pre-print is available [[Media:MPMea_2003.pdf|here]].<br />
<br />
* M. Clavel, J. Meseguer, and M. Palomino: [https://doi.org/10.1016/j.tcs.2006.12.009 Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic]. Theor. Comput. Sci. 373(1-2): 70-91 (2007)<br />
<br />
* P.C. Ölveczky and J. Meseguer: [https://doi.org/10.1007/s10990-007-9001-5 Semantics and pragmatics of Real-Time Maude]. High. Order Symb. Comput. 20(1-2): 161-196 (2007)<br />
<br />
* F. Durán and J. Meseguer: [https://doi.org/10.1016/j.scico.2006.07.002 Maude's module algebra]. Sci. Comput. Program. 66(2): 125-153 (2007)<br />
<br />
* R. Bruni and J. Meseguer: [https://doi.org/10.1016/j.tcs.2006.04.012 Semantic foundations for generalized rewrite theories]. Theor. Comput. Sci. 360(1-3): 386-414 (2006)<br />
<br />
* M. Clavel et al.: [https://doi.org/10.1016/S0304-3975(01)00359-0 Maude: specification and programming in rewriting logic]. Theor. Comput. Sci. 285(2): 187-243 (2002). A pre-print is available [[Media:CDELMMQspecprog_2001.pdf|here]].<br />
<br />
* J. Meseguer: [https://doi.org/10.1007/3-540-64299-4_26 Membership algebra as a logical framework for equational specification]. WADT: 18-61 (1997)<br />
<br />
* N. Martí-Oliet and J. Meseguer: [https://doi.org/10.1016/S1571-0661(04)00040-4 Rewriting logic as a logical and semantic framework]. WRLA: 190-225 (1996)<br />
<br />
* J. Meseguer: [https://www.sciencedirect.com/science/article/pii/030439759290182F Conditional rewriting logic as a unified model of concurrency]. Theor. Comput. Sci. 96(1): 73-155 (1996)<br />
<br />
Some interesting applications and uses of Maude:<br />
<br />
* S. Liu et al.: [https://dl.acm.org/doi/abs/10.1145/3603269.3604870 A Formal Framework for End-to-End DNS Resolution]. ACM SIGCOMM, pages 932–949 (2023)<br />
<br />
* S. Liu et al.: [https://doi.org/10.1145/3563299 Bridging the semantic gap between qualitative and quantitative models of distributed systems]. Proc. ACM Program. Lang. 6(OOPSLA2): 315-344 (2022)<br />
<br />
* P. Meredith et al. [doi: 10.1109/MEMCOD.2010.5558634 A formal executable semantics of Verilog] 8th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE) pp. 179-188 (2010)<br />
<br />
* P.C. Ölveczky, A. Boronat, and J. Meseguer: [https://doi.org/10.1007/978-3-642-13464-7_5 Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude]. Formal Techniques for Distributed Systems (FORTE), LNCS 6117 (2010)<br />
<br />
* S. Escobar, C. Meadows, and J. Meseguer: [https://doi.org/10.1007/978-3-642-03829-7_1 Maude-NPA: Cryptographic protocol analysis modulo equational properties] Foundations of Security Analysis and Design, LNCS 5705:1-50, Springer (2009)<br />
<br />
* J.E. Rivera, F. Durán, and A. Vallecillo: [doi:10.1177/0037549709341635 Formal Specification and Analysis of Domain Specific Models Using Maude]. SIMULATION. 85(11-12):778-792 (2009) <br />
<br />
* S. Chen et al.: [doi: 10.1109/SP.2007.6 A Systematic Approach to Uncover Security Flaws in GUI Logic] in IEEE Symposium on Security and Privacy (SP), pp. 71-85 (2007)<br />
<br />
* J.R. Romero et al.: [doi:10.5381/jot.2007.6.9.a10 Formal and Tool Support for Model Driven Engineering with Maude], Journal of Object Technology 6(9):187-207 (2007)<br />
<br />
* S. Escobar, C. Meadows, and J. Meseguer: [https://doi.org/10.1016/j.tcs.2006.08.035 A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties], TCS 367(1–2):162-202 (2006)<br />
<br />
* P.C. Ölveczky, J. Meseguer, and C.L. Talcott [https://doi.org/10.1007/s10703-006-0015-0 Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude]. Form Method Syst Des 29, 253–293 (2006)<br />
<br />
* G. Roşu and K. Havelund: [https://doi.org/10.1007/s10515-005-6205-y Rewriting-Based Techniques for Runtime Verification]. Autom Software Eng 12, 151–197 (2005)<br />
<br />
* A. Farzan et al.: [https://doi.org/10.1007/978-3-540-27813-9_46 Formal Analysis of Java Programs in JavaFAN]. Computer Aided Verification (CAV). LNCS 3114 (2004) <br />
<br />
* S. Eker et al.: [https://pubmed.ncbi.nlm.nih.gov/11928493/ Pathway logic: symbolic analysis of biological signaling]. Pac Symp Biocomput. 2002:400-12. (2002)<br />
<br />
* P. Degano, J. Meseguer, and U. Montanari, [doi: 10.1109/LICS.1989.39172 Axiomatizing net computations and processes] Fourth Annual Symposium on Logic in Computer Science, pp. 175-185 (1989)<br />
<br />
Some Additional Papers on Maude and on Rewriting Logic are available [http://maude.cs.illinois.edu/papers/ here].</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Rewriting_LogicRewriting Logic2023-10-11T08:21:03Z<p>Malaga: </p>
<hr />
<div><br />
The theory and applications of rewriting logic have been vigorously developed <br />
by researchers all over the world during the past years, with more than three <br />
hundred papers related to rewriting logic published so far <br />
(see the [[Roadmap and Bibliography|roadmap]]).<br />
<br />
International workshops on rewriting logic have been held in<br />
[http://www.sciencedirect.com/science/journal/15710661/4 United States (1996)], <br />
[http://www.sciencedirect.com/science/journal/15710661/15 France (1998)], <br />
[http://www.sciencedirect.com/science/journal/15710661/36 Japan (2000)], <br />
[http://www.sciencedirect.com/science/journal/15710661/71 Italy (2002)], <br />
[http://www.sciencedirect.com/science/journal/15710661/117 Spain (2004)],<br />
[http://www.sciencedirect.com/science/journal/15710661/176/4 Austria (2006)],<br />
[http://www.sciencedirect.com/science/journal/15710661/238/3 Hungary (2008)], <br />
[http://link.springer.com/book/10.1007/978-3-642-16310-4/page/1 Cyprus (2010)], <br />
[http://link.springer.com/book/10.1007/978-3-642-34005-5/page/1 Estonia (2012)], <br />
[http://users.dsic.upv.es/workshops/wrla2014/ France (2014)], <br />
[https://fmse.info.uaic.ro/events/WRLA2016/ The Netherlands (2016)], <br />
[https://project.inria.fr/wrla18/ Greece (2018)], <br />
[https://wrla2020.webs.upv.es/ Ireland (2020)],<br />
[http://sv.postech.ac.kr/wrla2022/ Germany (2022)].<br />
<br />
Several journal special issues have been published on rewriting logic:<br />
[https://www.sciencedirect.com/journal/theoretical-computer-science/vol/285/issue/2 TCS 285 (2002)],<br />
[https://link.springer.com/journal/10990/20/1/page/1 HOSC 20 (2007)],<br />
[https://www.sciencedirect.com/journal/the-journal-of-logic-and-algebraic-programming/vol/81 JLAMP 81 (2012)],<br />
[https://www.sciencedirect.com/journal/science-of-computer-programming/vol/99/ SCP 99 (2012)],<br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/vol/85/issue/1/part/P1 JLAMP 85 (2016)],<br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/vol/86/issue/1 JLAMP 86 (2017)], <br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/special-issue/10QHD3B3JSJ JLAMP 93 (2017)], <br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/special-issue/10R8T94S8FM JLAMP 110 (2020)], and <br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/special-issue/10HT7LGD2SQ JLAMP 134 (2023)].<br />
<br />
Furthermore, several language implementations of rewriting logic<br />
([http://www.ldl.jaist.ac.jp/cafeobj/index.html CafeOBJ], [http://elan.loria.fr/ ELAN], [[The Maude System|Maude]], etc.)<br />
and a variety of [[Maude Tools|formal tools]]<br />
have also been developed and have been used in a wide range of applications. <br />
You may take a look to the [https://doi.org/10.1007/978-3-030-17502-3_6 retrospective on rewrite engines published in TACAS 2019].<br />
<br />
Several snapshots of the state of rewriting logic research&mdash;some more global in scope, <br />
and others restricted to specific areas such as concurrency or object-based systems&mdash;have <br />
appeared so far<br />
[https://doi.org/10.1007/3-540-61604-7_64 CONCUR'96],<br />
[http://maude.cs.illinois.edu/papers/abstract/Mdirections_1998.html Marktoberdorf'98],<br />
[https://doi.org/10.1007/10721975_1 RTA'00],<br />
[https://doi.org/10.1007/978-0-387-35520-7_5 FMOODS'00], <br />
[http://maude.cs.illinois.edu/papers/abstract/MMroadmap_2001.html TCS'02],<br />
[https://doi.org/10.1016/j.jlap.2012.06.003 JLAMP'12], <br />
[https://doi.org/10.1007/978-3-662-57669-4_2 WoLLIC'18], <br />
[https://doi.org/10.1016/j.jlamp.2019.100497 JLAMP'20], and<br />
[https://doi.org/10.1007/978-3-031-10769-6_31 IJCAR'22].<br />
<br />
Maude should be seen as our contribution to the broader<br />
collective effort of building good language implementations for<br />
rewriting logic. In this regard, a key distinguishing feature of<br />
Maude is its systematic and efficient use of <EM>reflection</EM>,<br />
exploiting the fact that rewriting logic is reflective, a feature that<br />
makes Maude remarkably extensible and powerful, and that allows many<br />
advanced metaprogramming and metalanguage applications.<br />
<br />
Several versions of Maude have also been presented in different venues: <br />
[https://doi.org/10.1007/3-540-48685-2_18 RTA'99],<br />
[https://doi.org/10.1016/S1571-0661(05)80137-9 WRLA'00],<br />
[https://doi.org/10.1007/3-540-44881-0_7 RTA'03],<br />
[https://doi.org/10.1007/978-3-642-02348-4_27 RTA'04],<br />
[https://doi.org/10.4230/LIPIcs.RTA.2011.31 RTA'11], and<br />
[https://doi.org/10.1007/978-3-319-40229-1_13 IJCAR'16].<br />
An account of the history of the language may be found in the [https://doi.org/10.1007/978-3-319-23165-5_11 Two Decades of Maude] 2015 paper.<br />
Some more recent papers have focused on specific aspects of the language:<br />
[https://doi.org/10.1016/j.jlamp.2023.100887 strategies],<br />
[https://doi.org/10.1007/978-3-031-10769-6_31 symbolic features].</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Rewriting_LogicRewriting Logic2023-10-11T08:20:37Z<p>Malaga: </p>
<hr />
<div><br />
The theory and applications of rewriting logic have been vigorously developed <br />
by researchers all over the world during the past years, with more than three <br />
hundred papers related to rewriting logic published so far <br />
(see the [[Roadmap and Bibliography|roadmap]]).<br />
<br />
International workshops on rewriting logic have been held in<br />
[http://www.sciencedirect.com/science/journal/15710661/4 United States (1996)], <br />
[http://www.sciencedirect.com/science/journal/15710661/15 France (1998)], <br />
[http://www.sciencedirect.com/science/journal/15710661/36 Japan (2000)], <br />
[http://www.sciencedirect.com/science/journal/15710661/71 Italy (2002)], <br />
[http://www.sciencedirect.com/science/journal/15710661/117 Spain (2004)],<br />
[http://www.sciencedirect.com/science/journal/15710661/176/4 Austria (2006)],<br />
[http://www.sciencedirect.com/science/journal/15710661/238/3 Hungary (2008)], <br />
[http://link.springer.com/book/10.1007/978-3-642-16310-4/page/1 Cyprus (2010)], <br />
[http://link.springer.com/book/10.1007/978-3-642-34005-5/page/1 Estonia (2012)], <br />
[http://users.dsic.upv.es/workshops/wrla2014/ France (2014)], <br />
[https://fmse.info.uaic.ro/events/WRLA2016/ The Netherlands (2016)], <br />
[https://project.inria.fr/wrla18/ Greece (2018)], <br />
[https://wrla2020.webs.upv.es/ Ireland (2020)],<br />
[http://sv.postech.ac.kr/wrla2022/ Germany (2022)].<br />
<br />
Several journal special issues have been published on rewriting logic:<br />
[https://www.sciencedirect.com/journal/theoretical-computer-science/vol/285/issue/2 TCS 285 (2002)],<br />
[https://link.springer.com/journal/10990/20/1/page/1 HOSC 20 (2007)],<br />
[https://www.sciencedirect.com/journal/the-journal-of-logic-and-algebraic-programming/vol/81 JLAMP 81 (2012)],<br />
[https://www.sciencedirect.com/journal/science-of-computer-programming/vol/99/ SCP 99 (2012)],<br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/vol/85/issue/1/part/P1 JLAMP 85 (2016)],<br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/vol/86/issue/1 JLAMP 86 (2017)], <br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/special-issue/10QHD3B3JSJ JLAMP 93 (2017)], <br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/special-issue/10R8T94S8FM JLAMP 110 (2020)], and <br />
[https://www.sciencedirect.com/journal/journal-of-logical-and-algebraic-methods-in-programming/special-issue/10HT7LGD2SQ JLAMP 134 (2023).<br />
<br />
Furthermore, several language implementations of rewriting logic<br />
([http://www.ldl.jaist.ac.jp/cafeobj/index.html CafeOBJ], [http://elan.loria.fr/ ELAN], [[The Maude System|Maude]], etc.)<br />
and a variety of [[Maude Tools|formal tools]]<br />
have also been developed and have been used in a wide range of applications. <br />
You may take a look to the [https://doi.org/10.1007/978-3-030-17502-3_6 retrospective on rewrite engines published in TACAS 2019].<br />
<br />
Several snapshots of the state of rewriting logic research&mdash;some more global in scope, <br />
and others restricted to specific areas such as concurrency or object-based systems&mdash;have <br />
appeared so far<br />
[https://doi.org/10.1007/3-540-61604-7_64 CONCUR'96],<br />
[http://maude.cs.illinois.edu/papers/abstract/Mdirections_1998.html Marktoberdorf'98],<br />
[https://doi.org/10.1007/10721975_1 RTA'00],<br />
[https://doi.org/10.1007/978-0-387-35520-7_5 FMOODS'00], <br />
[http://maude.cs.illinois.edu/papers/abstract/MMroadmap_2001.html TCS'02],<br />
[https://doi.org/10.1016/j.jlap.2012.06.003 JLAMP'12], <br />
[https://doi.org/10.1007/978-3-662-57669-4_2 WoLLIC'18], <br />
[https://doi.org/10.1016/j.jlamp.2019.100497 JLAMP'20], and<br />
[https://doi.org/10.1007/978-3-031-10769-6_31 IJCAR'22].<br />
<br />
Maude should be seen as our contribution to the broader<br />
collective effort of building good language implementations for<br />
rewriting logic. In this regard, a key distinguishing feature of<br />
Maude is its systematic and efficient use of <EM>reflection</EM>,<br />
exploiting the fact that rewriting logic is reflective, a feature that<br />
makes Maude remarkably extensible and powerful, and that allows many<br />
advanced metaprogramming and metalanguage applications.<br />
<br />
Several versions of Maude have also been presented in different venues: <br />
[https://doi.org/10.1007/3-540-48685-2_18 RTA'99],<br />
[https://doi.org/10.1016/S1571-0661(05)80137-9 WRLA'00],<br />
[https://doi.org/10.1007/3-540-44881-0_7 RTA'03],<br />
[https://doi.org/10.1007/978-3-642-02348-4_27 RTA'04],<br />
[https://doi.org/10.4230/LIPIcs.RTA.2011.31 RTA'11], and<br />
[https://doi.org/10.1007/978-3-319-40229-1_13 IJCAR'16].<br />
An account of the history of the language may be found in the [https://doi.org/10.1007/978-3-319-23165-5_11 Two Decades of Maude] 2015 paper.<br />
Some more recent papers have focused on specific aspects of the language:<br />
[https://doi.org/10.1016/j.jlamp.2023.100887 strategies],<br />
[https://doi.org/10.1007/978-3-031-10769-6_31 symbolic features].</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Maude_download_and_installationMaude download and installation2023-04-20T06:34:27Z<p>Malaga: </p>
<hr />
<div>Maude 3.3.1 runs on many Unix variants, including Linux. The installations is straightforward, there is one single executable file with no dependencies whatsoever. Nevertheless, some hints on how to use it and how to install it in Windows platforms can be found [[installation guidelines|here]].<br />
<br />
In this section, we assume a Linux configuration. Please, substitute your platform name for 'linux' in what follows if you download for another platform. <br />
In any case, please consider subscribing to the [[Maude Mailing Lists|Maude users mailing list]], as this is also the mechanism by which we will make announcements about the system.<br />
<br />
The Maude system download consists of the Maude binaries, and documentation and examples.<br />
<br />
The Linux64 and macOS versions of Maude 3.3.1 are available at [https://github.com/SRI-CSL/Maude/releases/tag/Maude3.3.1 its GitHub site]. <br />
Its sources are available from the same place. You can find instructions together with the sources. <br />
<br />
To install from one of the above binaries, simply extract the downloaded zip file. This generates the folder with the following files in it:<br />
file.maude<br />
linear.maude<br />
machine-int.maude<br />
maude.[linux64|darwin64]<br />
metaInterpreter.maude<br />
model-checker.maude<br />
prelude.maude<br />
process.maude<br />
smt.maude<br />
socket.maude<br />
term-order.maude<br />
time.maude<br />
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude.linux64</tt> or <tt>maude.darwin64</tt>.<br />
<br />
== Maude manual and primer ==<br />
<br />
The manual for Maude 3.3.1 is available in [[Media:Maude-3.3.1-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The examples in the manual and in the book All About Maude is also available [[Media:Maude-3.3.1-manual-book-examples.zip|here]].<br />
<br />
== Main changes from Maude 3.3 to 3.3.1 ==<br />
<br />
* Some overparsing has been added to provide more informative hints on user input. <br />
* Some bugs fixed.<br />
<br />
== Main changes from Maude 3.2.2 to 3.3 ==<br />
<br />
* Support for object-oriented features, including object-oriented modules and theories. Classes and messages can now be declared in object-oriented modules and theories, with multiple inheritance and their semantics specified using object-oriented statements that are automatically completed to simplify the specification of object-oriented systems. The handling of object-oriented features has been implemented as syntactic sugar, once entered object-oriented modules and theories are transformed into corresponding system modules and theories. <br />
* The module system has been extended to support the new object-oriented features. Elements in object-oriented modules can be renamed when imported, and object-oriented parameterized modules can be instantiated using views from object-oriented theories. All other modules operations have been correspondingly extended. <br />
* Modules can now be imported in a new generated-by mode. <br />
* Some new commands and flags have been added. <br />
* Constants can be declared as parameters in theories, and be parameterized in parameterized modules. <br />
* Full Maude is no longer distributed as part of Maude. It is still available from the [https://github.com/maude-team/full-maude Full Maude's github site].<br />
* Some over parsing has been added to better recover and to provide more informative hints on user input. <br />
* Some bugs fixed.<br />
<br />
== Main changes from Maude 3.2 to 3.2.2 ==<br />
<br />
* Improvement on the vu-narrow command<br />
<br />
== Main changes from Maude 3.1 to 3.2 ==<br />
<br />
* Support for filtered variant unification in vu-narrow command,<br />
* Several improvements in unification modulo several axioms,<br />
* Several improvements of the external Maude I/O objects,<br />
* A command flag for the depth of searching for A/AU unifiers, and<br />
* Some bugs fixed.<br />
<br />
== Change list from Maude 3.0 to 3.1 ==<br />
<br />
* Support for unification modulo associativity-identity,<br />
* Support for the generation of irredundant unifiers, <br />
* Support for the filtering of variant unifiers using variant subsumption,<br />
* Support for the generation of variant matchers, <br />
* An implementation of Unix processes as Maude external objects,<br />
* Several improvements in the presentation of results, <br />
* Several improvements in the handling of control-c, <br />
* Some bugs fixed, and<br />
* Some improvements in syntax error detection and recovering.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Maude_download_and_installationMaude download and installation2023-04-19T18:05:14Z<p>Malaga: </p>
<hr />
<div>Maude 3.3.1 runs on many Unix variants, including Linux. The installations is straightforward, there is one single executable file with no dependencies whatsoever. Nevertheless, some hints on how to use it and how to install it in Windows platforms can be found [[installation guidelines|here]].<br />
<br />
In this section, we assume a Linux configuration. Please, substitute your platform name for 'linux' in what follows if you download for another platform. <br />
In any case, please consider subscribing to the [[Maude Mailing Lists|Maude users mailing list]], as this is also the mechanism by which we will make announcements about the system.<br />
<br />
The Maude system download consists of the Maude binaries, and documentation and examples.<br />
<br />
The Linux64 and macOS versions of Maude 3.3.1 are available at [https://github.com/SRI-CSL/Maude/releases/tag/3.3.1 its GitHub site]. <br />
Its sources are available from the same place. You can find instructions together with the sources. <br />
<br />
To install from one of the above binaries, simply extract the downloaded zip file. This generates the folder with the following files in it:<br />
file.maude<br />
linear.maude<br />
machine-int.maude<br />
maude.[linux64|darwin64]<br />
metaInterpreter.maude<br />
model-checker.maude<br />
prelude.maude<br />
process.maude<br />
smt.maude<br />
socket.maude<br />
term-order.maude<br />
time.maude<br />
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude.linux64</tt> or <tt>maude.darwin64</tt>.<br />
<br />
== Maude manual and primer ==<br />
<br />
The manual for Maude 3.3.1 is available in [[Media:Maude-3.3.1-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The examples in the manual and in the book All About Maude is also available [[Media:Maude-3.3.1-manual-book-examples.zip|here]].<br />
<br />
== Main changes from Maude 3.3 to 3.3.1 ==<br />
<br />
* Some overparsing has been added to provide more informative hints on user input. <br />
* Some bugs fixed.<br />
<br />
== Main changes from Maude 3.2.2 to 3.3 ==<br />
<br />
* Support for object-oriented features, including object-oriented modules and theories. Classes and messages can now be declared in object-oriented modules and theories, with multiple inheritance and their semantics specified using object-oriented statements that are automatically completed to simplify the specification of object-oriented systems. The handling of object-oriented features has been implemented as syntactic sugar, once entered object-oriented modules and theories are transformed into corresponding system modules and theories. <br />
* The module system has been extended to support the new object-oriented features. Elements in object-oriented modules can be renamed when imported, and object-oriented parameterized modules can be instantiated using views from object-oriented theories. All other modules operations have been correspondingly extended. <br />
* Modules can now be imported in a new generated-by mode. <br />
* Some new commands and flags have been added. <br />
* Constants can be declared as parameters in theories, and be parameterized in parameterized modules. <br />
* Full Maude is no longer distributed as part of Maude. It is still available from the [https://github.com/maude-team/full-maude Full Maude's github site].<br />
* Some over parsing has been added to better recover and to provide more informative hints on user input. <br />
* Some bugs fixed.<br />
<br />
== Main changes from Maude 3.2 to 3.2.2 ==<br />
<br />
* Improvement on the vu-narrow command<br />
<br />
== Main changes from Maude 3.1 to 3.2 ==<br />
<br />
* Support for filtered variant unification in vu-narrow command,<br />
* Several improvements in unification modulo several axioms,<br />
* Several improvements of the external Maude I/O objects,<br />
* A command flag for the depth of searching for A/AU unifiers, and<br />
* Some bugs fixed.<br />
<br />
== Change list from Maude 3.0 to 3.1 ==<br />
<br />
* Support for unification modulo associativity-identity,<br />
* Support for the generation of irredundant unifiers, <br />
* Support for the filtering of variant unifiers using variant subsumption,<br />
* Support for the generation of variant matchers, <br />
* An implementation of Unix processes as Maude external objects,<br />
* Several improvements in the presentation of results, <br />
* Several improvements in the handling of control-c, <br />
* Some bugs fixed, and<br />
* Some improvements in syntax error detection and recovering.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/All_Maude_3_versionsAll Maude 3 versions2023-04-19T17:58:52Z<p>Malaga: </p>
<hr />
<div>==Maude 3.2, 3.2.1, 3.2.2, 3.3, and 3.3.1==<br />
* Sources and binaries of all versions from 3.2 are available in [https://github.com/SRI-CSL/Maude/releases/ the releases section of its github repo].<br />
* Regarding the manual:<br />
- Manual for [https://maude.lcc.uma.es/maude321-manual-html/maude-manual.html Maude 3.2.1].<br />
- Manual for [https://maude.lcc.uma.es/maude32-manual-html/maude-manual.html Maude 3.2].<br />
<br />
==Maude 3.1==<br />
* [[Media:Maude-3.1-linux.zip|Maude 3.1 (with Yices 2) for Linux64]]<br />
* [[Media:Maude-3.1-macos.zip|Maude 3.1 (with Yices 2) for Mac OS X]]<br />
* [[Media:Maude-3.1.tar.gz|Maude 3.1 source files]]<br />
* [[Media:Full-Maude-3.1.zip|Full Maude 3.1]]<br />
* Maude 3.1 manual ([[Media:Maude-3.1-manual.pdf|pdf]]/[http://maude.lcc.uma.es/maude31-manual-html/maude-manual.html html]) and [[Media:Maude-3.1-manual-book-examples.zip|examples from the Maude 3.1 manual and book]]<br />
==Maude 3.0==<br />
* [[Media:Maude-3.0+yices2-linux.zip|Maude 3.0 (with Yices 2) for Linux64]]<br />
* [[Media:Maude-3.0+yices2-osx.zip|Maude 3.0 (with Yices 2) for Mac OS X]]<br />
* [[Media:Maude-3.0+cvc4-linux.zip|Maude 3.0 (with CVC 4) for Linux64]]<br />
* [[Media:Maude-3.0+cvc4-osx.zip|Maude 3.0 (with CVC 4) for Mac OS X]]<br />
* [[Media:Maude-3.0.tar.gz|Maude 3.0 source files]]<br />
* [[Media:Full-Maude-3.0.zip|Full Maude 3.0]]<br />
* Maude 3.0 manual ([[Media:Maude-3.0-manual.pdf|pdf]]/[http://maude.lcc.uma.es/maude30-manual-html/maude-manual.html html]) and [[Media:Maude-3.0-manual-book-examples.zip|examples from the Maude 3.0 manual and book]]</div>Malagahttps://maude.cs.illinois.edu/w/index.php/All_Maude_3_versionsAll Maude 3 versions2023-04-19T17:58:14Z<p>Malaga: /* Maude 3.2, 3.2.1, 3.2.2, 3.3, and 3.3.1 */</p>
<hr />
<div>==Maude 3.2, 3.2.1, 3.2.2, 3.3, and 3.3.1==<br />
* Sources and binaries of all versions from 3.2 are available in [https://github.com/SRI-CSL/Maude/releases/ the releases section of its github repo].<br />
* Regarding the manual:<br />
* [https://maude.lcc.uma.es/maude321-manual-html/maude-manual.html Maude 3.2.1]<br />
* [https://maude.lcc.uma.es/maude32-manual-html/maude-manual.html Maude 3.2]<br />
<br />
==Maude 3.1==<br />
* [[Media:Maude-3.1-linux.zip|Maude 3.1 (with Yices 2) for Linux64]]<br />
* [[Media:Maude-3.1-macos.zip|Maude 3.1 (with Yices 2) for Mac OS X]]<br />
* [[Media:Maude-3.1.tar.gz|Maude 3.1 source files]]<br />
* [[Media:Full-Maude-3.1.zip|Full Maude 3.1]]<br />
* Maude 3.1 manual ([[Media:Maude-3.1-manual.pdf|pdf]]/[http://maude.lcc.uma.es/maude31-manual-html/maude-manual.html html]) and [[Media:Maude-3.1-manual-book-examples.zip|examples from the Maude 3.1 manual and book]]<br />
==Maude 3.0==<br />
* [[Media:Maude-3.0+yices2-linux.zip|Maude 3.0 (with Yices 2) for Linux64]]<br />
* [[Media:Maude-3.0+yices2-osx.zip|Maude 3.0 (with Yices 2) for Mac OS X]]<br />
* [[Media:Maude-3.0+cvc4-linux.zip|Maude 3.0 (with CVC 4) for Linux64]]<br />
* [[Media:Maude-3.0+cvc4-osx.zip|Maude 3.0 (with CVC 4) for Mac OS X]]<br />
* [[Media:Maude-3.0.tar.gz|Maude 3.0 source files]]<br />
* [[Media:Full-Maude-3.0.zip|Full Maude 3.0]]<br />
* Maude 3.0 manual ([[Media:Maude-3.0-manual.pdf|pdf]]/[http://maude.lcc.uma.es/maude30-manual-html/maude-manual.html html]) and [[Media:Maude-3.0-manual-book-examples.zip|examples from the Maude 3.0 manual and book]]</div>Malagahttps://maude.cs.illinois.edu/w/index.php/All_Maude_3_versionsAll Maude 3 versions2023-04-19T17:57:40Z<p>Malaga: </p>
<hr />
<div>==Maude 3.2, 3.2.1, 3.2.2, 3.3, and 3.3.1==<br />
* Sources and binaries of all versions from 3.2 are available in [https://github.com/SRI-CSL/Maude/releases/ the releases section of its github repo].<br />
* Regarding the manual:<br />
* [https://maude.lcc.uma.es/maude321-manual-html/maude-manual.html Maude 3.2.1]<br />
* [https://maude.lcc.uma.es/maude32-manual-html/maude-manual.html Maude 3.2.1]<br />
<br />
==Maude 3.1==<br />
* [[Media:Maude-3.1-linux.zip|Maude 3.1 (with Yices 2) for Linux64]]<br />
* [[Media:Maude-3.1-macos.zip|Maude 3.1 (with Yices 2) for Mac OS X]]<br />
* [[Media:Maude-3.1.tar.gz|Maude 3.1 source files]]<br />
* [[Media:Full-Maude-3.1.zip|Full Maude 3.1]]<br />
* Maude 3.1 manual ([[Media:Maude-3.1-manual.pdf|pdf]]/[http://maude.lcc.uma.es/maude31-manual-html/maude-manual.html html]) and [[Media:Maude-3.1-manual-book-examples.zip|examples from the Maude 3.1 manual and book]]<br />
==Maude 3.0==<br />
* [[Media:Maude-3.0+yices2-linux.zip|Maude 3.0 (with Yices 2) for Linux64]]<br />
* [[Media:Maude-3.0+yices2-osx.zip|Maude 3.0 (with Yices 2) for Mac OS X]]<br />
* [[Media:Maude-3.0+cvc4-linux.zip|Maude 3.0 (with CVC 4) for Linux64]]<br />
* [[Media:Maude-3.0+cvc4-osx.zip|Maude 3.0 (with CVC 4) for Mac OS X]]<br />
* [[Media:Maude-3.0.tar.gz|Maude 3.0 source files]]<br />
* [[Media:Full-Maude-3.0.zip|Full Maude 3.0]]<br />
* Maude 3.0 manual ([[Media:Maude-3.0-manual.pdf|pdf]]/[http://maude.lcc.uma.es/maude30-manual-html/maude-manual.html html]) and [[Media:Maude-3.0-manual-book-examples.zip|examples from the Maude 3.0 manual and book]]</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Maude_download_and_installationMaude download and installation2023-04-19T17:51:44Z<p>Malaga: </p>
<hr />
<div>Maude 3.3.1 runs on many Unix variants, including Linux. The installations is straightforward, there is one single executable file with no dependencies whatsoever. Nevertheless, some hints on how to use it and how to install it in Windows platforms can be found [[installation guidelines|here]].<br />
<br />
In this section, we assume a Linux configuration. Please, substitute your platform name for 'linux' in what follows if you download for another platform. <br />
In any case, please consider subscribing to the [[Maude Mailing Lists|Maude users mailing list]], as this is also the mechanism by which we will make announcements about the system.<br />
<br />
The Maude system download consists of the Maude binaries, and documentation and examples.<br />
<br />
The Linux64 and macOS versions of Maude 3.3.1 are available at [https://github.com/SRI-CSL/Maude/releases/tag/3.3.1 its GitHub site]. <br />
Its sources are available from the same place. You can find instructions together with the sources. <br />
<br />
To install from one of the above binaries, simply extract the downloaded zip file. This generates the folder with the following files in it:<br />
file.maude<br />
linear.maude<br />
machine-int.maude<br />
maude.[linux64|darwin64]<br />
metaInterpreter.maude<br />
model-checker.maude<br />
prelude.maude<br />
process.maude<br />
smt.maude<br />
socket.maude<br />
term-order.maude<br />
time.maude<br />
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude.linux64</tt> or <tt>maude.darwin64</tt>.<br />
<br />
== Maude manual and primer ==<br />
<br />
The manual for Maude 3.3.1 is available in [[Media:Maude-3.3.1-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The examples in the manual and in the book All About Maude is also available [[Media:Maude-3.3.1-manual-book-examples.zip|here]].<br />
<br />
== Main changes from Maude 3.3 to 3.3.1 ==<br />
<br />
* Some overparsing has been added to provide more informative hints on user input. <br />
* Some bugs fixed.<br />
<br />
== Main changes from Maude 3.2.2 to 3.3 ==<br />
<br />
* Support for object-oriented features, including object-oriented modules and theories. Classes and messages can now be declared in object oriented modules and theories, with multiple inheritance and their semantics specified using object-oriented statements that are automatically completed to simplify the specification of object-oriented systems. The handling of object-oriented features has been implemented as syntactic sugar, once entered object-oriented modules and theories are transformed into corresponding system modules and theories. <br />
* The module system has been extended to support the new object-oriented features. Elements in object-oriented modules can be renamed, and object-oriented parameterized modules can be instantiated using views from object-oriented theories. <br />
* Some new commands and flags have been added. <br />
* Constants can be declared as parameters in theories, and be parameterized in parameterized modules. <br />
* Full Maude is no longer distributed as part of Maude. It is still available from the [https://github.com/maude-team/full-maude Full Maude's github site]<br />
* Some over parsing has been added to better recover and to provide more informative hints on user input. <br />
* Some bugs fixed.<br />
<br />
== Main changes from Maude 3.2 to 3.2.2 ==<br />
<br />
* Improvement on the vu-narrow command<br />
<br />
== Main changes from Maude 3.1 to 3.2 ==<br />
<br />
* Support for filtered variant unification in vu-narrow command,<br />
* Several improvements in unification modulo several axioms,<br />
* Several improvements of the external Maude I/O objects,<br />
* A command flag for the depth of searching for A/AU unifiers, and<br />
* Some bugs fixed.<br />
<br />
== Change list from Maude 3.0 to 3.1 ==<br />
<br />
* Support for unification modulo associativity-identity,<br />
* Support for the generation of irredundant unifiers, <br />
* Support for the filtering of variant unifiers using variant subsumption,<br />
* Support for the generation of variant matchers, <br />
* An implementation of Unix processes as Maude external objects,<br />
* Several improvements in the presentation of results, <br />
* Several improvements in the handling of control-c, <br />
* Some bugs fixed, and<br />
* Some improvements in syntax error detection and recovering.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Maude_download_and_installationMaude download and installation2023-04-19T17:42:39Z<p>Malaga: </p>
<hr />
<div>Maude 3.3.1 runs on many Unix variants, including Linux. The installations is straightforward, there is one single executable file with no dependencies whatsoever. Nevertheless, some hints on how to use it and how to install it in Windows platforms can be found [[installation guidelines|here]].<br />
<br />
In this section, we assume a Linux configuration. Please, substitute your platform name for 'linux' in what follows if you download for another platform. <br />
In any case, please consider subscribing to the [[Maude Mailing Lists|Maude users mailing list]], as this is also the mechanism by which we will make announcements about the system.<br />
<br />
The Maude system download consists of the Maude binaries, and documentation and examples.<br />
<br />
The Linux64 and macOS versions of Maude 3.3.1 are available at [https://github.com/SRI-CSL/Maude/releases/tag/3.3.1 its GitHub site]. <br />
Its sources are available from the same place. You can find instructions together with the sources. <br />
<br />
To install from one of the above binaries, simply extract the downloaded zip file. This generates the folder with the following files in it:<br />
file.maude<br />
linear.maude<br />
machine-int.maude<br />
maude.[linux64|darwin64]<br />
metaInterpreter.maude<br />
model-checker.maude<br />
prelude.maude<br />
process.maude<br />
smt.maude<br />
socket.maude<br />
term-order.maude<br />
time.maude<br />
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude.linux64</tt> or <tt>maude.darwin64</tt>.<br />
<br />
== Maude manual and primer ==<br />
<br />
The manual for Maude 3.3.1 is available in [[Media:Maude-3.3.1-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The examples in the manual and in the book All About Maude is also available [[Media:Maude-3.3.1-manual-book-examples.zip|here]].<br />
<br />
<br />
== Main changes from Maude 3.3 to 3.3.1 ==<br />
<br />
* Some overparsing has been added to provide more informative hints on user input. <br />
* Some bugs fixed.<br />
<br />
== Main changes from Maude 3.2.2 to 3.3 ==<br />
<br />
* Full Maude is no longer distributed as part of Maude. It is still available from the [https://github.com/maude-team/full-maude Full Maude's github site]<br />
* Some overparsing has been added to provide more informative hints on user input. <br />
* Some bugs fixed.<br />
<br />
== Main changes from Maude 3.2 to 3.2.2 ==<br />
<br />
* Improvement on the vu-narrow command<br />
<br />
== Main changes from Maude 3.1 to 3.2 ==<br />
<br />
* Support for filtered variant unification in vu-narrow command,<br />
* Several improvements in unification modulo several axioms,<br />
* Several improvements of the external Maude I/O objects,<br />
* A command flag for the depth of searching for A/AU unifiers, and<br />
* Some bugs fixed.<br />
<br />
== Change list from Maude 3.0 to 3.1 ==<br />
<br />
* Support for unification modulo associativity-identity,<br />
* Support for the generation of irredundant unifiers, <br />
* Support for the filtering of variant unifiers using variant subsumption,<br />
* Support for the generation of variant matchers, <br />
* An implementation of Unix processes as Maude external objects,<br />
* Several improvements in the presentation of results, <br />
* Several improvements in the handling of control-c, <br />
* Some bugs fixed, and<br />
* Some improvements in syntax error detection and recovering.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/File:Maude-3.3.1-manual-book-examples.zipFile:Maude-3.3.1-manual-book-examples.zip2023-04-19T16:52:39Z<p>Malaga: </p>
<hr />
<div></div>Malagahttps://maude.cs.illinois.edu/w/index.php/The_Maude_SystemThe Maude System2023-04-19T16:51:19Z<p>Malaga: Maude 3.3.1</p>
<hr />
<div><!--[[File:Maude-logo.png|right|400px]]--><br />
[[File:streets-cross.png|right|400px|thumb|link=https://www.google.com/maps/@37.392819,-122.0391638,3a,15y,246.71h,88.08t/data=!3m6!1e1!3m4!1sJ2um6VisMqkDoFT4Lpyd7A!2e0!7i16384!8i8192|[https://www.google.com/maps/@37.392819,-122.0391638,3a,15y,246.71h,88.08t/data=!3m6!1e1!3m4!1sJ2um6VisMqkDoFT4Lpyd7A!2e0!7i16384!8i8192 Streets cross at Sunnyvale, CA]]]<br />
<br />
== General Maude Information ==<br />
* [[Maude Overview]]<br />
* [[The Maude Project and Team]]<br />
* [[Rewriting Logic]]<br />
* [[Maude Mailing Addresses and Lists|Bug Reports and Mailing Lists]]<br />
<br />
== Maude Documentation ==<br />
<br />
* [[Maude Manual and Examples|Maude Manual and Examples]]<br />
* [[Some Papers on Maude and on Rewriting Logic|Some Papers on Maude and on Rewriting Logic]]<br />
<!-- * [http://maude.cs.illinois.edu/papers/ Some Papers on Maude and on Rewriting Logic] --><br />
<!-- * [[Roadmap and Bibliography]] --><br />
<!-- * [[Some Talks on Maude and on Rewriting Logic]] --><br />
<!-- * [[Maude 2 Primer and Examples|Maude Primer and Examples (not maintained)]] --><br />
<br />
== Maude-related Tools and Applications==<br />
* [[Maude Tools]]<br />
* [[Applications]]<br />
<br />
== Obtaining and Using Maude ==<br />
<br />
* [[Maude download and installation|Maude download and installation (Maude 3.3.1)]]<br />
* [[Maude License Agreement|Maude 3 License]]<br />
* [[All Maude 3 versions|All Maude 3 versions]]<br />
* [[All Maude 2 versions|All Maude 2 versions]]<br />
* [http://maude.cs.uiuc.edu/maude1/ Looking for Maude 1?]</div>Malagahttps://maude.cs.illinois.edu/w/index.php/File:Maude-3.3.1-manual.pdfFile:Maude-3.3.1-manual.pdf2023-04-19T16:49:58Z<p>Malaga: </p>
<hr />
<div></div>Malagahttps://maude.cs.illinois.edu/w/index.php/Maude_Manual_and_ExamplesMaude Manual and Examples2023-04-19T16:48:15Z<p>Malaga: </p>
<hr />
<div>== Manual - Latest Version ==<br />
<br />
The Maude manual for Maude 3.3.1 is available in [[Media:Maude-3.3.1-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude-manual HTML]. <br />
The source code for the examples used in the manual is also available [[Media:Maude-3.3.1-manual-book-examples.zip|here]] together with the examples from the Maude book.<br />
<br />
== Additional Resources ==<br />
<br />
Some papers a reports on Maude, its formal foundations, and its applications are available in the [[http://maude.cs.illinois.edu/w/index.php/Some_Papers_on_Maude_and_on_Rewriting_Logic Section on Some Papers on Maude and on Rewriting Logic]].<br />
A primer written for Maude 2.0.1 (but mostly applicable for later versions too) is available in [[Media:Maude-primer.pdf|PDF]] format. <br />
The examples are available as a tarred gzipped [[Media:Maude-primer-Ex.tar.gz|archive]].</div>Malagahttps://maude.cs.illinois.edu/w/index.php/File:Maude-3.2.1-manual.pdfFile:Maude-3.2.1-manual.pdf2023-03-16T11:39:17Z<p>Malaga: Malaga uploaded a new version of &quot;File:Maude-3.2.1-manual.pdf&quot;</p>
<hr />
<div></div>Malagahttps://maude.cs.illinois.edu/w/index.php/File:Maude-3.2.1-manual.pdfFile:Maude-3.2.1-manual.pdf2023-03-16T11:37:47Z<p>Malaga: Malaga uploaded a new version of &quot;File:Maude-3.2.1-manual.pdf&quot;</p>
<hr />
<div></div>Malagahttps://maude.cs.illinois.edu/w/index.php/Maude_download_and_installationMaude download and installation2023-02-09T18:32:55Z<p>Malaga: </p>
<hr />
<div>Maude 3.2.2 runs on many Unix variants, including Linux. The installations is straightforward, there is one single executable file with no dependencies whatsoever. Nevertheless, some hints on how to use it and how to install it in Windows platforms can be found [[installation guidelines|here]].<br />
<br />
In this section, we assume a Linux configuration. Please, substitute your platform name for 'linux' in what follows if you download for another platform. <br />
In any case, please consider subscribing to the [[Maude Mailing Lists|Maude users mailing list]], as this is also the mechanism by which we will make announcements about the system.<br />
<br />
The Maude system download consists of three parts: Core Maude, Full Maude, and documentation and examples.<br />
<br />
== Core Maude 3.2.2 ==<br />
<br />
The Linux64 and macOS versions of Maude 3.2.2 are available at [https://github.com/SRI-CSL/Maude/releases/tag/3.2.2 its GitHub site]. <br />
Its sources are available from the same place. You can find instructions together with the sources. <br />
<br />
To install from one of the above binaries, simply extract the downloaded zip file. This generates the folder with the following files in it:<br />
file.maude<br />
linear.maude<br />
machine-int.maude<br />
maude.[linux64|darwin64]<br />
metaInterpreter.maude<br />
model-checker.maude<br />
prelude.maude<br />
process.maude<br />
smt.maude<br />
socket.maude<br />
term-order.maude<br />
time.maude<br />
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude.linux64</tt> or <tt>maude.darwin64</tt>.<br />
<br />
== Full Maude 3.2.1 ==<br />
<br />
Full Maude is written in Maude, and is thus platform-independent. Download [[Media:Full-Maude-3.2.1.zip|Full Maude 3.2.1]] and save it into the Core Maude directory.<br />
<br />
== Maude manual and primer ==<br />
<br />
The manual for Maude 3.2.1 is available in [[Media:Maude-3.2.1-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude321-manual-html/maude-manual.html HTML]. <br />
The examples in the manual and in the book All About Maude is also available [[Media:Maude-3.1-manual-book-examples.zip|here]].<br />
<br />
== Main changes from Maude 3.2.2 to 3.2 ==<br />
<br />
* Improvement on the vu-narrow command<br />
<br />
== Main changes from Maude 3.1 to 3.2 ==<br />
<br />
* Support for filtered variant unification in vu-narrow command,<br />
* Several improvements in unification modulo several axioms,<br />
* Several improvements of the external Maude I/O objects,<br />
* A command flag for the depth of searching for A/AU unifiers, and<br />
* Some bugs fixed.<br />
<br />
== Change list from Maude 3.0 to 3.1 ==<br />
<br />
* Support for unification modulo associativity-identity,<br />
* Support for the generation of irredundant unifiers, <br />
* Support for the filtering of variant unifiers using variant subsumption,<br />
* Support for the generation of variant matchers, <br />
* An implementation of Unix processes as Maude external objects,<br />
* Several improvements in the presentation of results, <br />
* Several improvements in the handling of control-c, <br />
* Some bugs fixed, and<br />
* Some improvements in syntax error detection and recovering.</div>Malagahttps://maude.cs.illinois.edu/w/index.php/Maude_download_and_installationMaude download and installation2023-02-09T18:30:35Z<p>Malaga: </p>
<hr />
<div>Maude 3.2.2 runs on many Unix variants, including Linux. The installations is straightforward, there is one single executable file with no dependencies whatsoever. Nevertheless, some hints on how to use it and how to install it in Windows platforms can be found [[installation guidelines|here]].<br />
<br />
In this section, we assume a Linux configuration. Please, substitute your platform name for 'linux' in what follows if you download for another platform. <br />
In any case, please consider subscribing to the [[Maude Mailing Lists|Maude users mailing list]], as this is also the mechanism by which we will make announcements about the system.<br />
<br />
The Maude system download consists of three parts: Core Maude, Full Maude, and documentation and examples.<br />
<br />
== Core Maude 3.2.2 ==<br />
<br />
The Linux64 and macOS versions of Maude 3.2.2 are available at [https://github.com/SRI-CSL/Maude/releases/tag/3.2.2 its GitHub site]. <br />
Its sources are available from the same place. You can find instructions together with the sources. <br />
<br />
To install from one of the above binaries, simply extract the downloaded zip file. This generates the folder with the following files in it:<br />
file.maude<br />
linear.maude<br />
machine-int.maude<br />
maude.[linux64|darwin64]<br />
metaInterpreter.maude<br />
model-checker.maude<br />
prelude.maude<br />
process.maude<br />
smt.maude<br />
socket.maude<br />
term-order.maude<br />
time.maude<br />
Depending on your system you can now run Maude by starting the appropriate executable file: <tt>maude.linux64</tt> or <tt>maude.darwin64</tt>.<br />
<br />
== Full Maude 3.2.2 ==<br />
<br />
Full Maude is written in Maude, and is thus platform-independent. Download [[Media:Full-Maude-3.2.1.zip|Full Maude 3.2.2]] and save it into the Core Maude directory.<br />
<br />
== Maude manual and primer ==<br />
<br />
The manual for Maude 3.2.2 is available in [[Media:Maude-3.2.1-manual.pdf|PDF format]] and in [http://maude.lcc.uma.es/maude321-manual-html/maude-manual.html HTML]. <br />
The examples in the manual and in the book All About Maude is also available [[Media:Maude-3.1-manual-book-examples.zip|here]].<br />
<br />
== Main changes from Maude 3.2.2 to 3.2 ==<br />
<br />
* Improvement on the vu-narrow command<br />
<br />
== Main changes from Maude 3.1 to 3.2 ==<br />
<br />
* Support for filtered variant unification in vu-narrow command,<br />
* Several improvements in unification modulo several axioms,<br />
* Several improvements of the external Maude I/O objects,<br />
* A command flag for the depth of searching for A/AU unifiers, and<br />
* Some bugs fixed.<br />
<br />
== Change list from Maude 3.0 to 3.1 ==<br />
<br />
* Support for unification modulo associativity-identity,<br />
* Support for the generation of irredundant unifiers, <br />
* Support for the filtering of variant unifiers using variant subsumption,<br />
* Support for the generation of variant matchers, <br />
* An implementation of Unix processes as Maude external objects,<br />
* Several improvements in the presentation of results, <br />
* Several improvements in the handling of control-c, <br />
* Some bugs fixed, and<br />
* Some improvements in syntax error detection and recovering.</div>Malaga