As you probably can tell Maude sets out to solve a different set of problems than ordinary imperative languages. It is a formal reasoning tool, which can help us verify that things are "as they should", and show us why they are not if this is the case. Maude lets us define formally what we mean by some concept in a very abstract manner, but we can describe what is thought to be the equal concerning our theory (equations) and what state changes it can go through (rewrite rules). This is useful to validate security protocols and critical code. The Maude system has proved flaws in cryptography protocols by just specifying what the system can do , and by looking for unwanted situations the protocol can be showed to contain bugs, not programming bugs but situations happen that are hard to predict just by walking down the "happy path" as most developers do. We can use Maude's built-in search to look for unwanted states, or it can be used to show that no such states can be reached.
CiME 3 is a rewriting toolbox that provides Coq certificates for termination proofs (standard rewriting) obtained using various criteria: * Dependency pairs: o plain/marks, o graphs refinements with or without sub-term criterion, as well as various orderings: * Polynomial interpretations, * Matrix interpretations, * Full RPO with status, with AFS refinements. CiME 3 may be used alone (searching for proofs and producing certificates) or in conjunction with your own prover via xml input/output and translation to .v files. Note that in addition to its own xml format, CiME 3 now supports CPF for the aformentioned techniques.
H. Perez-Urbina, B. Motik, and I. Horrocks. Semantics in Data and Knowledge Bases, volume 4925 of Lecture Notes in Computer Science, page 199--214. Springer Berlin / Heidelberg, (2008)
S. Abiteboul, and O. Duschka. PODS '98: Proceedings of the seventeenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, page 254--263. New York, NY, USA, ACM, (1998)
H. Pérez-Urbina, I. Horrocks, and B. Motik. International Semantic Web Conference, volume 5823 of Lecture Notes in Computer Science, page 489-504. Springer, (2009)